open HolKernel boolLib bossLib Parse wordsLib;

(*
  wordsLib.output_words_as_hex();
*)

val _ = new_theory "tables";

val _ = computeLib.auto_import_definitions := false;

val Sbox_def = Define
  `Sbox (x:word8) = n2w (EL (w2n x)
    [0x63; 0x7C; 0x77; 0x7B; 0xF2; 0x6B; 0x6F; 0xC5;
     0x30; 0x01; 0x67; 0x2B; 0xFE; 0xD7; 0xAB; 0x76;
     0xCA; 0x82; 0xC9; 0x7D; 0xFA; 0x59; 0x47; 0xF0;
     0xAD; 0xD4; 0xA2; 0xAF; 0x9C; 0xA4; 0x72; 0xC0;
     0xB7; 0xFD; 0x93; 0x26; 0x36; 0x3F; 0xF7; 0xCC;
     0x34; 0xA5; 0xE5; 0xF1; 0x71; 0xD8; 0x31; 0x15;
     0x04; 0xC7; 0x23; 0xC3; 0x18; 0x96; 0x05; 0x9A;
     0x07; 0x12; 0x80; 0xE2; 0xEB; 0x27; 0xB2; 0x75;
     0x09; 0x83; 0x2C; 0x1A; 0x1B; 0x6E; 0x5A; 0xA0;
     0x52; 0x3B; 0xD6; 0xB3; 0x29; 0xE3; 0x2F; 0x84;
     0x53; 0xD1; 0x00; 0xED; 0x20; 0xFC; 0xB1; 0x5B;
     0x6A; 0xCB; 0xBE; 0x39; 0x4A; 0x4C; 0x58; 0xCF;
     0xD0; 0xEF; 0xAA; 0xFB; 0x43; 0x4D; 0x33; 0x85;
     0x45; 0xF9; 0x02; 0x7F; 0x50; 0x3C; 0x9F; 0xA8;
     0x51; 0xA3; 0x40; 0x8F; 0x92; 0x9D; 0x38; 0xF5;
     0xBC; 0xB6; 0xDA; 0x21; 0x10; 0xFF; 0xF3; 0xD2;
     0xCD; 0x0C; 0x13; 0xEC; 0x5F; 0x97; 0x44; 0x17;
     0xC4; 0xA7; 0x7E; 0x3D; 0x64; 0x5D; 0x19; 0x73;
     0x60; 0x81; 0x4F; 0xDC; 0x22; 0x2A; 0x90; 0x88;
     0x46; 0xEE; 0xB8; 0x14; 0xDE; 0x5E; 0x0B; 0xDB;
     0xE0; 0x32; 0x3A; 0x0A; 0x49; 0x06; 0x24; 0x5C;
     0xC2; 0xD3; 0xAC; 0x62; 0x91; 0x95; 0xE4; 0x79;
     0xE7; 0xC8; 0x37; 0x6D; 0x8D; 0xD5; 0x4E; 0xA9;
     0x6C; 0x56; 0xF4; 0xEA; 0x65; 0x7A; 0xAE; 0x08;
     0xBA; 0x78; 0x25; 0x2E; 0x1C; 0xA6; 0xB4; 0xC6;
     0xE8; 0xDD; 0x74; 0x1F; 0x4B; 0xBD; 0x8B; 0x8A;
     0x70; 0x3E; 0xB5; 0x66; 0x48; 0x03; 0xF6; 0x0E;
     0x61; 0x35; 0x57; 0xB9; 0x86; 0xC1; 0x1D; 0x9E;
     0xE1; 0xF8; 0x98; 0x11; 0x69; 0xD9; 0x8E; 0x94;
     0x9B; 0x1E; 0x87; 0xE9; 0xCE; 0x55; 0x28; 0xDF;
     0x8C; 0xA1; 0x89; 0x0D; 0xBF; 0xE6; 0x42; 0x68;
     0x41; 0x99; 0x2D; 0x0F; 0xB0; 0x54; 0xBB; 0x16]) : word8`;

val InvSbox_def = Define
  `InvSbox (x:word8) = n2w (EL (w2n x)
    [0x52; 0x09; 0x6A; 0xD5; 0x30; 0x36; 0xA5; 0x38;
     0xBF; 0x40; 0xA3; 0x9E; 0x81; 0xF3; 0xD7; 0xFB;
     0x7C; 0xE3; 0x39; 0x82; 0x9B; 0x2F; 0xFF; 0x87;
     0x34; 0x8E; 0x43; 0x44; 0xC4; 0xDE; 0xE9; 0xCB;
     0x54; 0x7B; 0x94; 0x32; 0xA6; 0xC2; 0x23; 0x3D;
     0xEE; 0x4C; 0x95; 0x0B; 0x42; 0xFA; 0xC3; 0x4E;
     0x08; 0x2E; 0xA1; 0x66; 0x28; 0xD9; 0x24; 0xB2;
     0x76; 0x5B; 0xA2; 0x49; 0x6D; 0x8B; 0xD1; 0x25;
     0x72; 0xF8; 0xF6; 0x64; 0x86; 0x68; 0x98; 0x16;
     0xD4; 0xA4; 0x5C; 0xCC; 0x5D; 0x65; 0xB6; 0x92;
     0x6C; 0x70; 0x48; 0x50; 0xFD; 0xED; 0xB9; 0xDA;
     0x5E; 0x15; 0x46; 0x57; 0xA7; 0x8D; 0x9D; 0x84;
     0x90; 0xD8; 0xAB; 0x00; 0x8C; 0xBC; 0xD3; 0x0A;
     0xF7; 0xE4; 0x58; 0x05; 0xB8; 0xB3; 0x45; 0x06;
     0xD0; 0x2C; 0x1E; 0x8F; 0xCA; 0x3F; 0x0F; 0x02;
     0xC1; 0xAF; 0xBD; 0x03; 0x01; 0x13; 0x8A; 0x6B;
     0x3A; 0x91; 0x11; 0x41; 0x4F; 0x67; 0xDC; 0xEA;
     0x97; 0xF2; 0xCF; 0xCE; 0xF0; 0xB4; 0xE6; 0x73;
     0x96; 0xAC; 0x74; 0x22; 0xE7; 0xAD; 0x35; 0x85;
     0xE2; 0xF9; 0x37; 0xE8; 0x1C; 0x75; 0xDF; 0x6E;
     0x47; 0xF1; 0x1A; 0x71; 0x1D; 0x29; 0xC5; 0x89;
     0x6F; 0xB7; 0x62; 0x0E; 0xAA; 0x18; 0xBE; 0x1B;
     0xFC; 0x56; 0x3E; 0x4B; 0xC6; 0xD2; 0x79; 0x20;
     0x9A; 0xDB; 0xC0; 0xFE; 0x78; 0xCD; 0x5A; 0xF4;
     0x1F; 0xDD; 0xA8; 0x33; 0x88; 0x07; 0xC7; 0x31;
     0xB1; 0x12; 0x10; 0x59; 0x27; 0x80; 0xEC; 0x5F;
     0x60; 0x51; 0x7F; 0xA9; 0x19; 0xB5; 0x4A; 0x0D;
     0x2D; 0xE5; 0x7A; 0x9F; 0x93; 0xC9; 0x9C; 0xEF;
     0xA0; 0xE0; 0x3B; 0x4D; 0xAE; 0x2A; 0xF5; 0xB0;
     0xC8; 0xEB; 0xBB; 0x3C; 0x83; 0x53; 0x99; 0x61;
     0x17; 0x2B; 0x04; 0x7E; 0xBA; 0x77; 0xD6; 0x26;
     0xE1; 0x69; 0x14; 0x63; 0x55; 0x21; 0x0C; 0x7D]) : word8`;

val Sbox = save_thm("Sbox",
  LIST_CONJ (map (REWRITE_CONV [Sbox_def] THENC EVAL) (for 0 255
    (fn i => ``Sbox (n2w ^(numSyntax.term_of_int i))``))));

val InvSbox = save_thm("InvSbox",
  LIST_CONJ (map (REWRITE_CONV [InvSbox_def] THENC EVAL) (for 0 255
    (fn i => ``InvSbox (n2w ^(numSyntax.term_of_int i))``))));

val _ = computeLib.add_persistent_funs ["Sbox", "InvSbox"];

val Sbox_Inversion = Q.store_thm
("Sbox_Inversion",
 `!w:word8. InvSbox (Sbox w) = w`,
 Cases_word_value THEN EVAL_TAC);

(*  The following has been superseded by the construction
    of tables in MultScript. We'll keep it for info purposes.

val GF256_by_2 = Count.apply word8Define
  `(GF256_by_2 0x0w = 0x0w) /\
   (GF256_by_2 0x1w = 0x2w) /\
   (GF256_by_2 0x2w = 0x4w) /\
   (GF256_by_2 0x3w = 0x6w) /\
   (GF256_by_2 0x4w = 0x8w) /\
   (GF256_by_2 0x5w = 0xAw) /\
   (GF256_by_2 0x6w = 0xCw) /\
   (GF256_by_2 0x7w = 0xEw) /\
   (GF256_by_2 0x8w = 0x10w) /\
   (GF256_by_2 0x9w = 0x12w) /\
   (GF256_by_2 0xAw = 0x14w) /\
   (GF256_by_2 0xBw = 0x16w) /\
   (GF256_by_2 0xCw = 0x18w) /\
   (GF256_by_2 0xDw = 0x1Aw) /\
   (GF256_by_2 0xEw = 0x1Cw) /\
   (GF256_by_2 0xFw = 0x1Ew) /\
   (GF256_by_2 0x10w = 0x20w) /\
   (GF256_by_2 0x11w = 0x22w) /\
   (GF256_by_2 0x12w = 0x24w) /\
   (GF256_by_2 0x13w = 0x26w) /\
   (GF256_by_2 0x14w = 0x28w) /\
   (GF256_by_2 0x15w = 0x2Aw) /\
   (GF256_by_2 0x16w = 0x2Cw) /\
   (GF256_by_2 0x17w = 0x2Ew) /\
   (GF256_by_2 0x18w = 0x30w) /\
   (GF256_by_2 0x19w = 0x32w) /\
   (GF256_by_2 0x1Aw = 0x34w) /\
   (GF256_by_2 0x1Bw = 0x36w) /\
   (GF256_by_2 0x1Cw = 0x38w) /\
   (GF256_by_2 0x1Dw = 0x3Aw) /\
   (GF256_by_2 0x1Ew = 0x3Cw) /\
   (GF256_by_2 0x1Fw = 0x3Ew) /\
   (GF256_by_2 0x20w = 0x40w) /\
   (GF256_by_2 0x21w = 0x42w) /\
   (GF256_by_2 0x22w = 0x44w) /\
   (GF256_by_2 0x23w = 0x46w) /\
   (GF256_by_2 0x24w = 0x48w) /\
   (GF256_by_2 0x25w = 0x4Aw) /\
   (GF256_by_2 0x26w = 0x4Cw) /\
   (GF256_by_2 0x27w = 0x4Ew) /\
   (GF256_by_2 0x28w = 0x50w) /\
   (GF256_by_2 0x29w = 0x52w) /\
   (GF256_by_2 0x2Aw = 0x54w) /\
   (GF256_by_2 0x2Bw = 0x56w) /\
   (GF256_by_2 0x2Cw = 0x58w) /\
   (GF256_by_2 0x2Dw = 0x5Aw) /\
   (GF256_by_2 0x2Ew = 0x5Cw) /\
   (GF256_by_2 0x2Fw = 0x5Ew) /\
   (GF256_by_2 0x30w = 0x60w) /\
   (GF256_by_2 0x31w = 0x62w) /\
   (GF256_by_2 0x32w = 0x64w) /\
   (GF256_by_2 0x33w = 0x66w) /\
   (GF256_by_2 0x34w = 0x68w) /\
   (GF256_by_2 0x35w = 0x6Aw) /\
   (GF256_by_2 0x36w = 0x6Cw) /\
   (GF256_by_2 0x37w = 0x6Ew) /\
   (GF256_by_2 0x38w = 0x70w) /\
   (GF256_by_2 0x39w = 0x72w) /\
   (GF256_by_2 0x3Aw = 0x74w) /\
   (GF256_by_2 0x3Bw = 0x76w) /\
   (GF256_by_2 0x3Cw = 0x78w) /\
   (GF256_by_2 0x3Dw = 0x7Aw) /\
   (GF256_by_2 0x3Ew = 0x7Cw) /\
   (GF256_by_2 0x3Fw = 0x7Ew) /\
   (GF256_by_2 0x40w = 0x80w) /\
   (GF256_by_2 0x41w = 0x82w) /\
   (GF256_by_2 0x42w = 0x84w) /\
   (GF256_by_2 0x43w = 0x86w) /\
   (GF256_by_2 0x44w = 0x88w) /\
   (GF256_by_2 0x45w = 0x8Aw) /\
   (GF256_by_2 0x46w = 0x8Cw) /\
   (GF256_by_2 0x47w = 0x8Ew) /\
   (GF256_by_2 0x48w = 0x90w) /\
   (GF256_by_2 0x49w = 0x92w) /\
   (GF256_by_2 0x4Aw = 0x94w) /\
   (GF256_by_2 0x4Bw = 0x96w) /\
   (GF256_by_2 0x4Cw = 0x98w) /\
   (GF256_by_2 0x4Dw = 0x9Aw) /\
   (GF256_by_2 0x4Ew = 0x9Cw) /\
   (GF256_by_2 0x4Fw = 0x9Ew) /\
   (GF256_by_2 0x50w = 0xA0w) /\
   (GF256_by_2 0x51w = 0xA2w) /\
   (GF256_by_2 0x52w = 0xA4w) /\
   (GF256_by_2 0x53w = 0xA6w) /\
   (GF256_by_2 0x54w = 0xA8w) /\
   (GF256_by_2 0x55w = 0xAAw) /\
   (GF256_by_2 0x56w = 0xACw) /\
   (GF256_by_2 0x57w = 0xAEw) /\
   (GF256_by_2 0x58w = 0xB0w) /\
   (GF256_by_2 0x59w = 0xB2w) /\
   (GF256_by_2 0x5Aw = 0xB4w) /\
   (GF256_by_2 0x5Bw = 0xB6w) /\
   (GF256_by_2 0x5Cw = 0xB8w) /\
   (GF256_by_2 0x5Dw = 0xBAw) /\
   (GF256_by_2 0x5Ew = 0xBCw) /\
   (GF256_by_2 0x5Fw = 0xBEw) /\
   (GF256_by_2 0x60w = 0xC0w) /\
   (GF256_by_2 0x61w = 0xC2w) /\
   (GF256_by_2 0x62w = 0xC4w) /\
   (GF256_by_2 0x63w = 0xC6w) /\
   (GF256_by_2 0x64w = 0xC8w) /\
   (GF256_by_2 0x65w = 0xCAw) /\
   (GF256_by_2 0x66w = 0xCCw) /\
   (GF256_by_2 0x67w = 0xCEw) /\
   (GF256_by_2 0x68w = 0xD0w) /\
   (GF256_by_2 0x69w = 0xD2w) /\
   (GF256_by_2 0x6Aw = 0xD4w) /\
   (GF256_by_2 0x6Bw = 0xD6w) /\
   (GF256_by_2 0x6Cw = 0xD8w) /\
   (GF256_by_2 0x6Dw = 0xDAw) /\
   (GF256_by_2 0x6Ew = 0xDCw) /\
   (GF256_by_2 0x6Fw = 0xDEw) /\
   (GF256_by_2 0x70w = 0xE0w) /\
   (GF256_by_2 0x71w = 0xE2w) /\
   (GF256_by_2 0x72w = 0xE4w) /\
   (GF256_by_2 0x73w = 0xE6w) /\
   (GF256_by_2 0x74w = 0xE8w) /\
   (GF256_by_2 0x75w = 0xEAw) /\
   (GF256_by_2 0x76w = 0xECw) /\
   (GF256_by_2 0x77w = 0xEEw) /\
   (GF256_by_2 0x78w = 0xF0w) /\
   (GF256_by_2 0x79w = 0xF2w) /\
   (GF256_by_2 0x7Aw = 0xF4w) /\
   (GF256_by_2 0x7Bw = 0xF6w) /\
   (GF256_by_2 0x7Cw = 0xF8w) /\
   (GF256_by_2 0x7Dw = 0xFAw) /\
   (GF256_by_2 0x7Ew = 0xFCw) /\
   (GF256_by_2 0x7Fw = 0xFEw) /\
   (GF256_by_2 0x80w = 0x1Bw) /\
   (GF256_by_2 0x81w = 0x19w) /\
   (GF256_by_2 0x82w = 0x1Fw) /\
   (GF256_by_2 0x83w = 0x1Dw) /\
   (GF256_by_2 0x84w = 0x13w) /\
   (GF256_by_2 0x85w = 0x11w) /\
   (GF256_by_2 0x86w = 0x17w) /\
   (GF256_by_2 0x87w = 0x15w) /\
   (GF256_by_2 0x88w = 0xBw)  /\
   (GF256_by_2 0x89w = 0x9w)  /\
   (GF256_by_2 0x8Aw = 0xFw)  /\
   (GF256_by_2 0x8Bw = 0xDw)  /\
   (GF256_by_2 0x8Cw = 0x3w)  /\
   (GF256_by_2 0x8Dw = 0x1w)  /\
   (GF256_by_2 0x8Ew = 0x7w)  /\
   (GF256_by_2 0x8Fw = 0x5w)  /\
   (GF256_by_2 0x90w = 0x3Bw) /\
   (GF256_by_2 0x91w = 0x39w) /\
   (GF256_by_2 0x92w = 0x3Fw) /\
   (GF256_by_2 0x93w = 0x3Dw) /\
   (GF256_by_2 0x94w = 0x33w) /\
   (GF256_by_2 0x95w = 0x31w) /\
   (GF256_by_2 0x96w = 0x37w) /\
   (GF256_by_2 0x97w = 0x35w) /\
   (GF256_by_2 0x98w = 0x2Bw) /\
   (GF256_by_2 0x99w = 0x29w) /\
   (GF256_by_2 0x9Aw = 0x2Fw) /\
   (GF256_by_2 0x9Bw = 0x2Dw) /\
   (GF256_by_2 0x9Cw = 0x23w) /\
   (GF256_by_2 0x9Dw = 0x21w) /\
   (GF256_by_2 0x9Ew = 0x27w) /\
   (GF256_by_2 0x9Fw = 0x25w) /\
   (GF256_by_2 0xA0w = 0x5Bw) /\
   (GF256_by_2 0xA1w = 0x59w) /\
   (GF256_by_2 0xA2w = 0x5Fw) /\
   (GF256_by_2 0xA3w = 0x5Dw) /\
   (GF256_by_2 0xA4w = 0x53w) /\
   (GF256_by_2 0xA5w = 0x51w) /\
   (GF256_by_2 0xA6w = 0x57w) /\
   (GF256_by_2 0xA7w = 0x55w) /\
   (GF256_by_2 0xA8w = 0x4Bw) /\
   (GF256_by_2 0xA9w = 0x49w) /\
   (GF256_by_2 0xAAw = 0x4Fw) /\
   (GF256_by_2 0xABw = 0x4Dw) /\
   (GF256_by_2 0xACw = 0x43w) /\
   (GF256_by_2 0xADw = 0x41w) /\
   (GF256_by_2 0xAEw = 0x47w) /\
   (GF256_by_2 0xAFw = 0x45w) /\
   (GF256_by_2 0xB0w = 0x7Bw) /\
   (GF256_by_2 0xB1w = 0x79w) /\
   (GF256_by_2 0xB2w = 0x7Fw) /\
   (GF256_by_2 0xB3w = 0x7Dw) /\
   (GF256_by_2 0xB4w = 0x73w) /\
   (GF256_by_2 0xB5w = 0x71w) /\
   (GF256_by_2 0xB6w = 0x77w) /\
   (GF256_by_2 0xB7w = 0x75w) /\
   (GF256_by_2 0xB8w = 0x6Bw) /\
   (GF256_by_2 0xB9w = 0x69w) /\
   (GF256_by_2 0xBAw = 0x6Fw) /\
   (GF256_by_2 0xBBw = 0x6Dw) /\
   (GF256_by_2 0xBCw = 0x63w) /\
   (GF256_by_2 0xBDw = 0x61w) /\
   (GF256_by_2 0xBEw = 0x67w) /\
   (GF256_by_2 0xBFw = 0x65w) /\
   (GF256_by_2 0xC0w = 0x9Bw) /\
   (GF256_by_2 0xC1w = 0x99w) /\
   (GF256_by_2 0xC2w = 0x9Fw) /\
   (GF256_by_2 0xC3w = 0x9Dw) /\
   (GF256_by_2 0xC4w = 0x93w) /\
   (GF256_by_2 0xC5w = 0x91w) /\
   (GF256_by_2 0xC6w = 0x97w) /\
   (GF256_by_2 0xC7w = 0x95w) /\
   (GF256_by_2 0xC8w = 0x8Bw) /\
   (GF256_by_2 0xC9w = 0x89w) /\
   (GF256_by_2 0xCAw = 0x8Fw) /\
   (GF256_by_2 0xCBw = 0x8Dw) /\
   (GF256_by_2 0xCCw = 0x83w) /\
   (GF256_by_2 0xCDw = 0x81w) /\
   (GF256_by_2 0xCEw = 0x87w) /\
   (GF256_by_2 0xCFw = 0x85w) /\
   (GF256_by_2 0xD0w = 0xBBw) /\
   (GF256_by_2 0xD1w = 0xB9w) /\
   (GF256_by_2 0xD2w = 0xBFw) /\
   (GF256_by_2 0xD3w = 0xBDw) /\
   (GF256_by_2 0xD4w = 0xB3w) /\
   (GF256_by_2 0xD5w = 0xB1w) /\
   (GF256_by_2 0xD6w = 0xB7w) /\
   (GF256_by_2 0xD7w = 0xB5w) /\
   (GF256_by_2 0xD8w = 0xABw) /\
   (GF256_by_2 0xD9w = 0xA9w) /\
   (GF256_by_2 0xDAw = 0xAFw) /\
   (GF256_by_2 0xDBw = 0xADw) /\
   (GF256_by_2 0xDCw = 0xA3w) /\
   (GF256_by_2 0xDDw = 0xA1w) /\
   (GF256_by_2 0xDEw = 0xA7w) /\
   (GF256_by_2 0xDFw = 0xA5w) /\
   (GF256_by_2 0xE0w = 0xDBw) /\
   (GF256_by_2 0xE1w = 0xD9w) /\
   (GF256_by_2 0xE2w = 0xDFw) /\
   (GF256_by_2 0xE3w = 0xDDw) /\
   (GF256_by_2 0xE4w = 0xD3w) /\
   (GF256_by_2 0xE5w = 0xD1w) /\
   (GF256_by_2 0xE6w = 0xD7w) /\
   (GF256_by_2 0xE7w = 0xD5w) /\
   (GF256_by_2 0xE8w = 0xCBw) /\
   (GF256_by_2 0xE9w = 0xC9w) /\
   (GF256_by_2 0xEAw = 0xCFw) /\
   (GF256_by_2 0xEBw = 0xCDw) /\
   (GF256_by_2 0xECw = 0xC3w) /\
   (GF256_by_2 0xEDw = 0xC1w) /\
   (GF256_by_2 0xEEw = 0xC7w) /\
   (GF256_by_2 0xEFw = 0xC5w) /\
   (GF256_by_2 0xF0w = 0xFBw) /\
   (GF256_by_2 0xF1w = 0xF9w) /\
   (GF256_by_2 0xF2w = 0xFFw) /\
   (GF256_by_2 0xF3w = 0xFDw) /\
   (GF256_by_2 0xF4w = 0xF3w) /\
   (GF256_by_2 0xF5w = 0xF1w) /\
   (GF256_by_2 0xF6w = 0xF7w) /\
   (GF256_by_2 0xF7w = 0xF5w) /\
   (GF256_by_2 0xF8w = 0xEBw) /\
   (GF256_by_2 0xF9w = 0xE9w) /\
   (GF256_by_2 0xFAw = 0xEFw) /\
   (GF256_by_2 0xFBw = 0xEDw) /\
   (GF256_by_2 0xFCw = 0xE3w) /\
   (GF256_by_2 0xFDw = 0xE1w) /\
   (GF256_by_2 0xFEw = 0xE7w) /\
   (GF256_by_2 0xFFw = 0xE5w)`;

val GF256_by_3 = Count.apply word8Define
  `(GF256_by_3 0x0w = 0x0w) /\
   (GF256_by_3 0x1w = 0x3w) /\
   (GF256_by_3 0x2w = 0x6w) /\
   (GF256_by_3 0x3w = 0x5w) /\
   (GF256_by_3 0x4w = 0xCw) /\
   (GF256_by_3 0x5w = 0xFw) /\
   (GF256_by_3 0x6w = 0xAw) /\
   (GF256_by_3 0x7w = 0x9w) /\
   (GF256_by_3 0x8w = 0x18w) /\
   (GF256_by_3 0x9w = 0x1Bw) /\
   (GF256_by_3 0xAw = 0x1Ew) /\
   (GF256_by_3 0xBw = 0x1Dw) /\
   (GF256_by_3 0xCw = 0x14w) /\
   (GF256_by_3 0xDw = 0x17w) /\
   (GF256_by_3 0xEw = 0x12w) /\
   (GF256_by_3 0xFw = 0x11w) /\
   (GF256_by_3 0x10w = 0x30w) /\
   (GF256_by_3 0x11w = 0x33w) /\
   (GF256_by_3 0x12w = 0x36w) /\
   (GF256_by_3 0x13w = 0x35w) /\
   (GF256_by_3 0x14w = 0x3Cw) /\
   (GF256_by_3 0x15w = 0x3Fw) /\
   (GF256_by_3 0x16w = 0x3Aw) /\
   (GF256_by_3 0x17w = 0x39w) /\
   (GF256_by_3 0x18w = 0x28w) /\
   (GF256_by_3 0x19w = 0x2Bw) /\
   (GF256_by_3 0x1Aw = 0x2Ew) /\
   (GF256_by_3 0x1Bw = 0x2Dw) /\
   (GF256_by_3 0x1Cw = 0x24w) /\
   (GF256_by_3 0x1Dw = 0x27w) /\
   (GF256_by_3 0x1Ew = 0x22w) /\
   (GF256_by_3 0x1Fw = 0x21w) /\
   (GF256_by_3 0x20w = 0x60w) /\
   (GF256_by_3 0x21w = 0x63w) /\
   (GF256_by_3 0x22w = 0x66w) /\
   (GF256_by_3 0x23w = 0x65w) /\
   (GF256_by_3 0x24w = 0x6Cw) /\
   (GF256_by_3 0x25w = 0x6Fw) /\
   (GF256_by_3 0x26w = 0x6Aw) /\
   (GF256_by_3 0x27w = 0x69w) /\
   (GF256_by_3 0x28w = 0x78w) /\
   (GF256_by_3 0x29w = 0x7Bw) /\
   (GF256_by_3 0x2Aw = 0x7Ew) /\
   (GF256_by_3 0x2Bw = 0x7Dw) /\
   (GF256_by_3 0x2Cw = 0x74w) /\
   (GF256_by_3 0x2Dw = 0x77w) /\
   (GF256_by_3 0x2Ew = 0x72w) /\
   (GF256_by_3 0x2Fw = 0x71w) /\
   (GF256_by_3 0x30w = 0x50w) /\
   (GF256_by_3 0x31w = 0x53w) /\
   (GF256_by_3 0x32w = 0x56w) /\
   (GF256_by_3 0x33w = 0x55w) /\
   (GF256_by_3 0x34w = 0x5Cw) /\
   (GF256_by_3 0x35w = 0x5Fw) /\
   (GF256_by_3 0x36w = 0x5Aw) /\
   (GF256_by_3 0x37w = 0x59w) /\
   (GF256_by_3 0x38w = 0x48w) /\
   (GF256_by_3 0x39w = 0x4Bw) /\
   (GF256_by_3 0x3Aw = 0x4Ew) /\
   (GF256_by_3 0x3Bw = 0x4Dw) /\
   (GF256_by_3 0x3Cw = 0x44w) /\
   (GF256_by_3 0x3Dw = 0x47w) /\
   (GF256_by_3 0x3Ew = 0x42w) /\
   (GF256_by_3 0x3Fw = 0x41w) /\
   (GF256_by_3 0x40w = 0xC0w) /\
   (GF256_by_3 0x41w = 0xC3w) /\
   (GF256_by_3 0x42w = 0xC6w) /\
   (GF256_by_3 0x43w = 0xC5w) /\
   (GF256_by_3 0x44w = 0xCCw) /\
   (GF256_by_3 0x45w = 0xCFw) /\
   (GF256_by_3 0x46w = 0xCAw) /\
   (GF256_by_3 0x47w = 0xC9w) /\
   (GF256_by_3 0x48w = 0xD8w) /\
   (GF256_by_3 0x49w = 0xDBw) /\
   (GF256_by_3 0x4Aw = 0xDEw) /\
   (GF256_by_3 0x4Bw = 0xDDw) /\
   (GF256_by_3 0x4Cw = 0xD4w) /\
   (GF256_by_3 0x4Dw = 0xD7w) /\
   (GF256_by_3 0x4Ew = 0xD2w) /\
   (GF256_by_3 0x4Fw = 0xD1w) /\
   (GF256_by_3 0x50w = 0xF0w) /\
   (GF256_by_3 0x51w = 0xF3w) /\
   (GF256_by_3 0x52w = 0xF6w) /\
   (GF256_by_3 0x53w = 0xF5w) /\
   (GF256_by_3 0x54w = 0xFCw) /\
   (GF256_by_3 0x55w = 0xFFw) /\
   (GF256_by_3 0x56w = 0xFAw) /\
   (GF256_by_3 0x57w = 0xF9w) /\
   (GF256_by_3 0x58w = 0xE8w) /\
   (GF256_by_3 0x59w = 0xEBw) /\
   (GF256_by_3 0x5Aw = 0xEEw) /\
   (GF256_by_3 0x5Bw = 0xEDw) /\
   (GF256_by_3 0x5Cw = 0xE4w) /\
   (GF256_by_3 0x5Dw = 0xE7w) /\
   (GF256_by_3 0x5Ew = 0xE2w) /\
   (GF256_by_3 0x5Fw = 0xE1w) /\
   (GF256_by_3 0x60w = 0xA0w) /\
   (GF256_by_3 0x61w = 0xA3w) /\
   (GF256_by_3 0x62w = 0xA6w) /\
   (GF256_by_3 0x63w = 0xA5w) /\
   (GF256_by_3 0x64w = 0xACw) /\
   (GF256_by_3 0x65w = 0xAFw) /\
   (GF256_by_3 0x66w = 0xAAw) /\
   (GF256_by_3 0x67w = 0xA9w) /\
   (GF256_by_3 0x68w = 0xB8w) /\
   (GF256_by_3 0x69w = 0xBBw) /\
   (GF256_by_3 0x6Aw = 0xBEw) /\
   (GF256_by_3 0x6Bw = 0xBDw) /\
   (GF256_by_3 0x6Cw = 0xB4w) /\
   (GF256_by_3 0x6Dw = 0xB7w) /\
   (GF256_by_3 0x6Ew = 0xB2w) /\
   (GF256_by_3 0x6Fw = 0xB1w) /\
   (GF256_by_3 0x70w = 0x90w) /\
   (GF256_by_3 0x71w = 0x93w) /\
   (GF256_by_3 0x72w = 0x96w) /\
   (GF256_by_3 0x73w = 0x95w) /\
   (GF256_by_3 0x74w = 0x9Cw) /\
   (GF256_by_3 0x75w = 0x9Fw) /\
   (GF256_by_3 0x76w = 0x9Aw) /\
   (GF256_by_3 0x77w = 0x99w) /\
   (GF256_by_3 0x78w = 0x88w) /\
   (GF256_by_3 0x79w = 0x8Bw) /\
   (GF256_by_3 0x7Aw = 0x8Ew) /\
   (GF256_by_3 0x7Bw = 0x8Dw) /\
   (GF256_by_3 0x7Cw = 0x84w) /\
   (GF256_by_3 0x7Dw = 0x87w) /\
   (GF256_by_3 0x7Ew = 0x82w) /\
   (GF256_by_3 0x7Fw = 0x81w) /\
   (GF256_by_3 0x80w = 0x9Bw) /\
   (GF256_by_3 0x81w = 0x98w) /\
   (GF256_by_3 0x82w = 0x9Dw) /\
   (GF256_by_3 0x83w = 0x9Ew) /\
   (GF256_by_3 0x84w = 0x97w) /\
   (GF256_by_3 0x85w = 0x94w) /\
   (GF256_by_3 0x86w = 0x91w) /\
   (GF256_by_3 0x87w = 0x92w) /\
   (GF256_by_3 0x88w = 0x83w) /\
   (GF256_by_3 0x89w = 0x80w) /\
   (GF256_by_3 0x8Aw = 0x85w) /\
   (GF256_by_3 0x8Bw = 0x86w) /\
   (GF256_by_3 0x8Cw = 0x8Fw) /\
   (GF256_by_3 0x8Dw = 0x8Cw) /\
   (GF256_by_3 0x8Ew = 0x89w) /\
   (GF256_by_3 0x8Fw = 0x8Aw) /\
   (GF256_by_3 0x90w = 0xABw) /\
   (GF256_by_3 0x91w = 0xA8w) /\
   (GF256_by_3 0x92w = 0xADw) /\
   (GF256_by_3 0x93w = 0xAEw) /\
   (GF256_by_3 0x94w = 0xA7w) /\
   (GF256_by_3 0x95w = 0xA4w) /\
   (GF256_by_3 0x96w = 0xA1w) /\
   (GF256_by_3 0x97w = 0xA2w) /\
   (GF256_by_3 0x98w = 0xB3w) /\
   (GF256_by_3 0x99w = 0xB0w) /\
   (GF256_by_3 0x9Aw = 0xB5w) /\
   (GF256_by_3 0x9Bw = 0xB6w) /\
   (GF256_by_3 0x9Cw = 0xBFw) /\
   (GF256_by_3 0x9Dw = 0xBCw) /\
   (GF256_by_3 0x9Ew = 0xB9w) /\
   (GF256_by_3 0x9Fw = 0xBAw) /\
   (GF256_by_3 0xA0w = 0xFBw) /\
   (GF256_by_3 0xA1w = 0xF8w) /\
   (GF256_by_3 0xA2w = 0xFDw) /\
   (GF256_by_3 0xA3w = 0xFEw) /\
   (GF256_by_3 0xA4w = 0xF7w) /\
   (GF256_by_3 0xA5w = 0xF4w) /\
   (GF256_by_3 0xA6w = 0xF1w) /\
   (GF256_by_3 0xA7w = 0xF2w) /\
   (GF256_by_3 0xA8w = 0xE3w) /\
   (GF256_by_3 0xA9w = 0xE0w) /\
   (GF256_by_3 0xAAw = 0xE5w) /\
   (GF256_by_3 0xABw = 0xE6w) /\
   (GF256_by_3 0xACw = 0xEFw) /\
   (GF256_by_3 0xADw = 0xECw) /\
   (GF256_by_3 0xAEw = 0xE9w) /\
   (GF256_by_3 0xAFw = 0xEAw) /\
   (GF256_by_3 0xB0w = 0xCBw) /\
   (GF256_by_3 0xB1w = 0xC8w) /\
   (GF256_by_3 0xB2w = 0xCDw) /\
   (GF256_by_3 0xB3w = 0xCEw) /\
   (GF256_by_3 0xB4w = 0xC7w) /\
   (GF256_by_3 0xB5w = 0xC4w) /\
   (GF256_by_3 0xB6w = 0xC1w) /\
   (GF256_by_3 0xB7w = 0xC2w) /\
   (GF256_by_3 0xB8w = 0xD3w) /\
   (GF256_by_3 0xB9w = 0xD0w) /\
   (GF256_by_3 0xBAw = 0xD5w) /\
   (GF256_by_3 0xBBw = 0xD6w) /\
   (GF256_by_3 0xBCw = 0xDFw) /\
   (GF256_by_3 0xBDw = 0xDCw) /\
   (GF256_by_3 0xBEw = 0xD9w) /\
   (GF256_by_3 0xBFw = 0xDAw) /\
   (GF256_by_3 0xC0w = 0x5Bw) /\
   (GF256_by_3 0xC1w = 0x58w) /\
   (GF256_by_3 0xC2w = 0x5Dw) /\
   (GF256_by_3 0xC3w = 0x5Ew) /\
   (GF256_by_3 0xC4w = 0x57w) /\
   (GF256_by_3 0xC5w = 0x54w) /\
   (GF256_by_3 0xC6w = 0x51w) /\
   (GF256_by_3 0xC7w = 0x52w) /\
   (GF256_by_3 0xC8w = 0x43w) /\
   (GF256_by_3 0xC9w = 0x40w) /\
   (GF256_by_3 0xCAw = 0x45w) /\
   (GF256_by_3 0xCBw = 0x46w) /\
   (GF256_by_3 0xCCw = 0x4Fw) /\
   (GF256_by_3 0xCDw = 0x4Cw) /\
   (GF256_by_3 0xCEw = 0x49w) /\
   (GF256_by_3 0xCFw = 0x4Aw) /\
   (GF256_by_3 0xD0w = 0x6Bw) /\
   (GF256_by_3 0xD1w = 0x68w) /\
   (GF256_by_3 0xD2w = 0x6Dw) /\
   (GF256_by_3 0xD3w = 0x6Ew) /\
   (GF256_by_3 0xD4w = 0x67w) /\
   (GF256_by_3 0xD5w = 0x64w) /\
   (GF256_by_3 0xD6w = 0x61w) /\
   (GF256_by_3 0xD7w = 0x62w) /\
   (GF256_by_3 0xD8w = 0x73w) /\
   (GF256_by_3 0xD9w = 0x70w) /\
   (GF256_by_3 0xDAw = 0x75w) /\
   (GF256_by_3 0xDBw = 0x76w) /\
   (GF256_by_3 0xDCw = 0x7Fw) /\
   (GF256_by_3 0xDDw = 0x7Cw) /\
   (GF256_by_3 0xDEw = 0x79w) /\
   (GF256_by_3 0xDFw = 0x7Aw) /\
   (GF256_by_3 0xE0w = 0x3Bw) /\
   (GF256_by_3 0xE1w = 0x38w) /\
   (GF256_by_3 0xE2w = 0x3Dw) /\
   (GF256_by_3 0xE3w = 0x3Ew) /\
   (GF256_by_3 0xE4w = 0x37w) /\
   (GF256_by_3 0xE5w = 0x34w) /\
   (GF256_by_3 0xE6w = 0x31w) /\
   (GF256_by_3 0xE7w = 0x32w) /\
   (GF256_by_3 0xE8w = 0x23w) /\
   (GF256_by_3 0xE9w = 0x20w) /\
   (GF256_by_3 0xEAw = 0x25w) /\
   (GF256_by_3 0xEBw = 0x26w) /\
   (GF256_by_3 0xECw = 0x2Fw) /\
   (GF256_by_3 0xEDw = 0x2Cw) /\
   (GF256_by_3 0xEEw = 0x29w) /\
   (GF256_by_3 0xEFw = 0x2Aw) /\
   (GF256_by_3 0xF0w = 0xBw)  /\
   (GF256_by_3 0xF1w = 0x8w)  /\
   (GF256_by_3 0xF2w = 0xDw)  /\
   (GF256_by_3 0xF3w = 0xEw)  /\
   (GF256_by_3 0xF4w = 0x7w)  /\
   (GF256_by_3 0xF5w = 0x4w)  /\
   (GF256_by_3 0xF6w = 0x1w)  /\
   (GF256_by_3 0xF7w = 0x2w)  /\
   (GF256_by_3 0xF8w = 0x13w) /\
   (GF256_by_3 0xF9w = 0x10w) /\
   (GF256_by_3 0xFAw = 0x15w) /\
   (GF256_by_3 0xFBw = 0x16w) /\
   (GF256_by_3 0xFCw = 0x1Fw) /\
   (GF256_by_3 0xFDw = 0x1Cw) /\
   (GF256_by_3 0xFEw = 0x19w) /\
   (GF256_by_3 0xFFw = 0x1Aw)`;

val GF256_by_9 = Count.apply word8Define
  `(GF256_by_9 0x0w = 0x0w)  /\
   (GF256_by_9 0x1w = 0x9w)  /\
   (GF256_by_9 0x2w = 0x12w) /\
   (GF256_by_9 0x3w = 0x1Bw) /\
   (GF256_by_9 0x4w = 0x24w) /\
   (GF256_by_9 0x5w = 0x2Dw) /\
   (GF256_by_9 0x6w = 0x36w) /\
   (GF256_by_9 0x7w = 0x3Fw) /\
   (GF256_by_9 0x8w = 0x48w) /\
   (GF256_by_9 0x9w = 0x41w) /\
   (GF256_by_9 0xAw = 0x5Aw) /\
   (GF256_by_9 0xBw = 0x53w) /\
   (GF256_by_9 0xCw = 0x6Cw) /\
   (GF256_by_9 0xDw = 0x65w) /\
   (GF256_by_9 0xEw = 0x7Ew) /\
   (GF256_by_9 0xFw = 0x77w) /\
   (GF256_by_9 0x10w = 0x90w) /\
   (GF256_by_9 0x11w = 0x99w) /\
   (GF256_by_9 0x12w = 0x82w) /\
   (GF256_by_9 0x13w = 0x8Bw) /\
   (GF256_by_9 0x14w = 0xB4w) /\
   (GF256_by_9 0x15w = 0xBDw) /\
   (GF256_by_9 0x16w = 0xA6w) /\
   (GF256_by_9 0x17w = 0xAFw) /\
   (GF256_by_9 0x18w = 0xD8w) /\
   (GF256_by_9 0x19w = 0xD1w) /\
   (GF256_by_9 0x1Aw = 0xCAw) /\
   (GF256_by_9 0x1Bw = 0xC3w) /\
   (GF256_by_9 0x1Cw = 0xFCw) /\
   (GF256_by_9 0x1Dw = 0xF5w) /\
   (GF256_by_9 0x1Ew = 0xEEw) /\
   (GF256_by_9 0x1Fw = 0xE7w) /\
   (GF256_by_9 0x20w = 0x3Bw) /\
   (GF256_by_9 0x21w = 0x32w) /\
   (GF256_by_9 0x22w = 0x29w) /\
   (GF256_by_9 0x23w = 0x20w) /\
   (GF256_by_9 0x24w = 0x1Fw) /\
   (GF256_by_9 0x25w = 0x16w) /\
   (GF256_by_9 0x26w = 0xDw)  /\
   (GF256_by_9 0x27w = 0x4w)  /\
   (GF256_by_9 0x28w = 0x73w) /\
   (GF256_by_9 0x29w = 0x7Aw) /\
   (GF256_by_9 0x2Aw = 0x61w) /\
   (GF256_by_9 0x2Bw = 0x68w) /\
   (GF256_by_9 0x2Cw = 0x57w) /\
   (GF256_by_9 0x2Dw = 0x5Ew) /\
   (GF256_by_9 0x2Ew = 0x45w) /\
   (GF256_by_9 0x2Fw = 0x4Cw) /\
   (GF256_by_9 0x30w = 0xABw) /\
   (GF256_by_9 0x31w = 0xA2w) /\
   (GF256_by_9 0x32w = 0xB9w) /\
   (GF256_by_9 0x33w = 0xB0w) /\
   (GF256_by_9 0x34w = 0x8Fw) /\
   (GF256_by_9 0x35w = 0x86w) /\
   (GF256_by_9 0x36w = 0x9Dw) /\
   (GF256_by_9 0x37w = 0x94w) /\
   (GF256_by_9 0x38w = 0xE3w) /\
   (GF256_by_9 0x39w = 0xEAw) /\
   (GF256_by_9 0x3Aw = 0xF1w) /\
   (GF256_by_9 0x3Bw = 0xF8w) /\
   (GF256_by_9 0x3Cw = 0xC7w) /\
   (GF256_by_9 0x3Dw = 0xCEw) /\
   (GF256_by_9 0x3Ew = 0xD5w) /\
   (GF256_by_9 0x3Fw = 0xDCw) /\
   (GF256_by_9 0x40w = 0x76w) /\
   (GF256_by_9 0x41w = 0x7Fw) /\
   (GF256_by_9 0x42w = 0x64w) /\
   (GF256_by_9 0x43w = 0x6Dw) /\
   (GF256_by_9 0x44w = 0x52w) /\
   (GF256_by_9 0x45w = 0x5Bw) /\
   (GF256_by_9 0x46w = 0x40w) /\
   (GF256_by_9 0x47w = 0x49w) /\
   (GF256_by_9 0x48w = 0x3Ew) /\
   (GF256_by_9 0x49w = 0x37w) /\
   (GF256_by_9 0x4Aw = 0x2Cw) /\
   (GF256_by_9 0x4Bw = 0x25w) /\
   (GF256_by_9 0x4Cw = 0x1Aw) /\
   (GF256_by_9 0x4Dw = 0x13w) /\
   (GF256_by_9 0x4Ew = 0x8w)  /\
   (GF256_by_9 0x4Fw = 0x1w)  /\
   (GF256_by_9 0x50w = 0xE6w) /\
   (GF256_by_9 0x51w = 0xEFw) /\
   (GF256_by_9 0x52w = 0xF4w) /\
   (GF256_by_9 0x53w = 0xFDw) /\
   (GF256_by_9 0x54w = 0xC2w) /\
   (GF256_by_9 0x55w = 0xCBw) /\
   (GF256_by_9 0x56w = 0xD0w) /\
   (GF256_by_9 0x57w = 0xD9w) /\
   (GF256_by_9 0x58w = 0xAEw) /\
   (GF256_by_9 0x59w = 0xA7w) /\
   (GF256_by_9 0x5Aw = 0xBCw) /\
   (GF256_by_9 0x5Bw = 0xB5w) /\
   (GF256_by_9 0x5Cw = 0x8Aw) /\
   (GF256_by_9 0x5Dw = 0x83w) /\
   (GF256_by_9 0x5Ew = 0x98w) /\
   (GF256_by_9 0x5Fw = 0x91w) /\
   (GF256_by_9 0x60w = 0x4Dw) /\
   (GF256_by_9 0x61w = 0x44w) /\
   (GF256_by_9 0x62w = 0x5Fw) /\
   (GF256_by_9 0x63w = 0x56w) /\
   (GF256_by_9 0x64w = 0x69w) /\
   (GF256_by_9 0x65w = 0x60w) /\
   (GF256_by_9 0x66w = 0x7Bw) /\
   (GF256_by_9 0x67w = 0x72w) /\
   (GF256_by_9 0x68w = 0x5w)  /\
   (GF256_by_9 0x69w = 0xCw)  /\
   (GF256_by_9 0x6Aw = 0x17w) /\
   (GF256_by_9 0x6Bw = 0x1Ew) /\
   (GF256_by_9 0x6Cw = 0x21w) /\
   (GF256_by_9 0x6Dw = 0x28w) /\
   (GF256_by_9 0x6Ew = 0x33w) /\
   (GF256_by_9 0x6Fw = 0x3Aw) /\
   (GF256_by_9 0x70w = 0xDDw) /\
   (GF256_by_9 0x71w = 0xD4w) /\
   (GF256_by_9 0x72w = 0xCFw) /\
   (GF256_by_9 0x73w = 0xC6w) /\
   (GF256_by_9 0x74w = 0xF9w) /\
   (GF256_by_9 0x75w = 0xF0w) /\
   (GF256_by_9 0x76w = 0xEBw) /\
   (GF256_by_9 0x77w = 0xE2w) /\
   (GF256_by_9 0x78w = 0x95w) /\
   (GF256_by_9 0x79w = 0x9Cw) /\
   (GF256_by_9 0x7Aw = 0x87w) /\
   (GF256_by_9 0x7Bw = 0x8Ew) /\
   (GF256_by_9 0x7Cw = 0xB1w) /\
   (GF256_by_9 0x7Dw = 0xB8w) /\
   (GF256_by_9 0x7Ew = 0xA3w) /\
   (GF256_by_9 0x7Fw = 0xAAw) /\
   (GF256_by_9 0x80w = 0xECw) /\
   (GF256_by_9 0x81w = 0xE5w) /\
   (GF256_by_9 0x82w = 0xFEw) /\
   (GF256_by_9 0x83w = 0xF7w) /\
   (GF256_by_9 0x84w = 0xC8w) /\
   (GF256_by_9 0x85w = 0xC1w) /\
   (GF256_by_9 0x86w = 0xDAw) /\
   (GF256_by_9 0x87w = 0xD3w) /\
   (GF256_by_9 0x88w = 0xA4w) /\
   (GF256_by_9 0x89w = 0xADw) /\
   (GF256_by_9 0x8Aw = 0xB6w) /\
   (GF256_by_9 0x8Bw = 0xBFw) /\
   (GF256_by_9 0x8Cw = 0x80w) /\
   (GF256_by_9 0x8Dw = 0x89w) /\
   (GF256_by_9 0x8Ew = 0x92w) /\
   (GF256_by_9 0x8Fw = 0x9Bw) /\
   (GF256_by_9 0x90w = 0x7Cw) /\
   (GF256_by_9 0x91w = 0x75w) /\
   (GF256_by_9 0x92w = 0x6Ew) /\
   (GF256_by_9 0x93w = 0x67w) /\
   (GF256_by_9 0x94w = 0x58w) /\
   (GF256_by_9 0x95w = 0x51w) /\
   (GF256_by_9 0x96w = 0x4Aw) /\
   (GF256_by_9 0x97w = 0x43w) /\
   (GF256_by_9 0x98w = 0x34w) /\
   (GF256_by_9 0x99w = 0x3Dw) /\
   (GF256_by_9 0x9Aw = 0x26w) /\
   (GF256_by_9 0x9Bw = 0x2Fw) /\
   (GF256_by_9 0x9Cw = 0x10w) /\
   (GF256_by_9 0x9Dw = 0x19w) /\
   (GF256_by_9 0x9Ew = 0x2w)  /\
   (GF256_by_9 0x9Fw = 0xBw)  /\
   (GF256_by_9 0xA0w = 0xD7w) /\
   (GF256_by_9 0xA1w = 0xDEw) /\
   (GF256_by_9 0xA2w = 0xC5w) /\
   (GF256_by_9 0xA3w = 0xCCw) /\
   (GF256_by_9 0xA4w = 0xF3w) /\
   (GF256_by_9 0xA5w = 0xFAw) /\
   (GF256_by_9 0xA6w = 0xE1w) /\
   (GF256_by_9 0xA7w = 0xE8w) /\
   (GF256_by_9 0xA8w = 0x9Fw) /\
   (GF256_by_9 0xA9w = 0x96w) /\
   (GF256_by_9 0xAAw = 0x8Dw) /\
   (GF256_by_9 0xABw = 0x84w) /\
   (GF256_by_9 0xACw = 0xBBw) /\
   (GF256_by_9 0xADw = 0xB2w) /\
   (GF256_by_9 0xAEw = 0xA9w) /\
   (GF256_by_9 0xAFw = 0xA0w) /\
   (GF256_by_9 0xB0w = 0x47w) /\
   (GF256_by_9 0xB1w = 0x4Ew) /\
   (GF256_by_9 0xB2w = 0x55w) /\
   (GF256_by_9 0xB3w = 0x5Cw) /\
   (GF256_by_9 0xB4w = 0x63w) /\
   (GF256_by_9 0xB5w = 0x6Aw) /\
   (GF256_by_9 0xB6w = 0x71w) /\
   (GF256_by_9 0xB7w = 0x78w) /\
   (GF256_by_9 0xB8w = 0xFw)  /\
   (GF256_by_9 0xB9w = 0x6w)  /\
   (GF256_by_9 0xBAw = 0x1Dw) /\
   (GF256_by_9 0xBBw = 0x14w) /\
   (GF256_by_9 0xBCw = 0x2Bw) /\
   (GF256_by_9 0xBDw = 0x22w) /\
   (GF256_by_9 0xBEw = 0x39w) /\
   (GF256_by_9 0xBFw = 0x30w) /\
   (GF256_by_9 0xC0w = 0x9Aw) /\
   (GF256_by_9 0xC1w = 0x93w) /\
   (GF256_by_9 0xC2w = 0x88w) /\
   (GF256_by_9 0xC3w = 0x81w) /\
   (GF256_by_9 0xC4w = 0xBEw) /\
   (GF256_by_9 0xC5w = 0xB7w) /\
   (GF256_by_9 0xC6w = 0xACw) /\
   (GF256_by_9 0xC7w = 0xA5w) /\
   (GF256_by_9 0xC8w = 0xD2w) /\
   (GF256_by_9 0xC9w = 0xDBw) /\
   (GF256_by_9 0xCAw = 0xC0w) /\
   (GF256_by_9 0xCBw = 0xC9w) /\
   (GF256_by_9 0xCCw = 0xF6w) /\
   (GF256_by_9 0xCDw = 0xFFw) /\
   (GF256_by_9 0xCEw = 0xE4w) /\
   (GF256_by_9 0xCFw = 0xEDw) /\
   (GF256_by_9 0xD0w = 0xAw)  /\
   (GF256_by_9 0xD1w = 0x3w)  /\
   (GF256_by_9 0xD2w = 0x18w) /\
   (GF256_by_9 0xD3w = 0x11w) /\
   (GF256_by_9 0xD4w = 0x2Ew) /\
   (GF256_by_9 0xD5w = 0x27w) /\
   (GF256_by_9 0xD6w = 0x3Cw) /\
   (GF256_by_9 0xD7w = 0x35w) /\
   (GF256_by_9 0xD8w = 0x42w) /\
   (GF256_by_9 0xD9w = 0x4Bw) /\
   (GF256_by_9 0xDAw = 0x50w) /\
   (GF256_by_9 0xDBw = 0x59w) /\
   (GF256_by_9 0xDCw = 0x66w) /\
   (GF256_by_9 0xDDw = 0x6Fw) /\
   (GF256_by_9 0xDEw = 0x74w) /\
   (GF256_by_9 0xDFw = 0x7Dw) /\
   (GF256_by_9 0xE0w = 0xA1w) /\
   (GF256_by_9 0xE1w = 0xA8w) /\
   (GF256_by_9 0xE2w = 0xB3w) /\
   (GF256_by_9 0xE3w = 0xBAw) /\
   (GF256_by_9 0xE4w = 0x85w) /\
   (GF256_by_9 0xE5w = 0x8Cw) /\
   (GF256_by_9 0xE6w = 0x97w) /\
   (GF256_by_9 0xE7w = 0x9Ew) /\
   (GF256_by_9 0xE8w = 0xE9w) /\
   (GF256_by_9 0xE9w = 0xE0w) /\
   (GF256_by_9 0xEAw = 0xFBw) /\
   (GF256_by_9 0xEBw = 0xF2w) /\
   (GF256_by_9 0xECw = 0xCDw) /\
   (GF256_by_9 0xEDw = 0xC4w) /\
   (GF256_by_9 0xEEw = 0xDFw) /\
   (GF256_by_9 0xEFw = 0xD6w) /\
   (GF256_by_9 0xF0w = 0x31w) /\
   (GF256_by_9 0xF1w = 0x38w) /\
   (GF256_by_9 0xF2w = 0x23w) /\
   (GF256_by_9 0xF3w = 0x2Aw) /\
   (GF256_by_9 0xF4w = 0x15w) /\
   (GF256_by_9 0xF5w = 0x1Cw) /\
   (GF256_by_9 0xF6w = 0x7w)  /\
   (GF256_by_9 0xF7w = 0xEw)  /\
   (GF256_by_9 0xF8w = 0x79w) /\
   (GF256_by_9 0xF9w = 0x70w) /\
   (GF256_by_9 0xFAw = 0x6Bw) /\
   (GF256_by_9 0xFBw = 0x62w) /\
   (GF256_by_9 0xFCw = 0x5Dw) /\
   (GF256_by_9 0xFDw = 0x54w) /\
   (GF256_by_9 0xFEw = 0x4Fw) /\
   (GF256_by_9 0xFFw = 0x46w)`;

val GF256_by_11 = Count.apply word8Define
  `(GF256_by_11 0x0w = 0x0w)  /\
   (GF256_by_11 0x1w = 0xBw)  /\
   (GF256_by_11 0x2w = 0x16w) /\
   (GF256_by_11 0x3w = 0x1Dw) /\
   (GF256_by_11 0x4w = 0x2Cw) /\
   (GF256_by_11 0x5w = 0x27w) /\
   (GF256_by_11 0x6w = 0x3Aw) /\
   (GF256_by_11 0x7w = 0x31w) /\
   (GF256_by_11 0x8w = 0x58w) /\
   (GF256_by_11 0x9w = 0x53w) /\
   (GF256_by_11 0xAw = 0x4Ew) /\
   (GF256_by_11 0xBw = 0x45w) /\
   (GF256_by_11 0xCw = 0x74w) /\
   (GF256_by_11 0xDw = 0x7Fw) /\
   (GF256_by_11 0xEw = 0x62w) /\
   (GF256_by_11 0xFw = 0x69w) /\
   (GF256_by_11 0x10w = 0xB0w) /\
   (GF256_by_11 0x11w = 0xBBw) /\
   (GF256_by_11 0x12w = 0xA6w) /\
   (GF256_by_11 0x13w = 0xADw) /\
   (GF256_by_11 0x14w = 0x9Cw) /\
   (GF256_by_11 0x15w = 0x97w) /\
   (GF256_by_11 0x16w = 0x8Aw) /\
   (GF256_by_11 0x17w = 0x81w) /\
   (GF256_by_11 0x18w = 0xE8w) /\
   (GF256_by_11 0x19w = 0xE3w) /\
   (GF256_by_11 0x1Aw = 0xFEw) /\
   (GF256_by_11 0x1Bw = 0xF5w) /\
   (GF256_by_11 0x1Cw = 0xC4w) /\
   (GF256_by_11 0x1Dw = 0xCFw) /\
   (GF256_by_11 0x1Ew = 0xD2w) /\
   (GF256_by_11 0x1Fw = 0xD9w) /\
   (GF256_by_11 0x20w = 0x7Bw) /\
   (GF256_by_11 0x21w = 0x70w) /\
   (GF256_by_11 0x22w = 0x6Dw) /\
   (GF256_by_11 0x23w = 0x66w) /\
   (GF256_by_11 0x24w = 0x57w) /\
   (GF256_by_11 0x25w = 0x5Cw) /\
   (GF256_by_11 0x26w = 0x41w) /\
   (GF256_by_11 0x27w = 0x4Aw) /\
   (GF256_by_11 0x28w = 0x23w) /\
   (GF256_by_11 0x29w = 0x28w) /\
   (GF256_by_11 0x2Aw = 0x35w) /\
   (GF256_by_11 0x2Bw = 0x3Ew) /\
   (GF256_by_11 0x2Cw = 0xFw)  /\
   (GF256_by_11 0x2Dw = 0x4w)  /\
   (GF256_by_11 0x2Ew = 0x19w) /\
   (GF256_by_11 0x2Fw = 0x12w) /\
   (GF256_by_11 0x30w = 0xCBw) /\
   (GF256_by_11 0x31w = 0xC0w) /\
   (GF256_by_11 0x32w = 0xDDw) /\
   (GF256_by_11 0x33w = 0xD6w) /\
   (GF256_by_11 0x34w = 0xE7w) /\
   (GF256_by_11 0x35w = 0xECw) /\
   (GF256_by_11 0x36w = 0xF1w) /\
   (GF256_by_11 0x37w = 0xFAw) /\
   (GF256_by_11 0x38w = 0x93w) /\
   (GF256_by_11 0x39w = 0x98w) /\
   (GF256_by_11 0x3Aw = 0x85w) /\
   (GF256_by_11 0x3Bw = 0x8Ew) /\
   (GF256_by_11 0x3Cw = 0xBFw) /\
   (GF256_by_11 0x3Dw = 0xB4w) /\
   (GF256_by_11 0x3Ew = 0xA9w) /\
   (GF256_by_11 0x3Fw = 0xA2w) /\
   (GF256_by_11 0x40w = 0xF6w) /\
   (GF256_by_11 0x41w = 0xFDw) /\
   (GF256_by_11 0x42w = 0xE0w) /\
   (GF256_by_11 0x43w = 0xEBw) /\
   (GF256_by_11 0x44w = 0xDAw) /\
   (GF256_by_11 0x45w = 0xD1w) /\
   (GF256_by_11 0x46w = 0xCCw) /\
   (GF256_by_11 0x47w = 0xC7w) /\
   (GF256_by_11 0x48w = 0xAEw) /\
   (GF256_by_11 0x49w = 0xA5w) /\
   (GF256_by_11 0x4Aw = 0xB8w) /\
   (GF256_by_11 0x4Bw = 0xB3w) /\
   (GF256_by_11 0x4Cw = 0x82w) /\
   (GF256_by_11 0x4Dw = 0x89w) /\
   (GF256_by_11 0x4Ew = 0x94w) /\
   (GF256_by_11 0x4Fw = 0x9Fw) /\
   (GF256_by_11 0x50w = 0x46w) /\
   (GF256_by_11 0x51w = 0x4Dw) /\
   (GF256_by_11 0x52w = 0x50w) /\
   (GF256_by_11 0x53w = 0x5Bw) /\
   (GF256_by_11 0x54w = 0x6Aw) /\
   (GF256_by_11 0x55w = 0x61w) /\
   (GF256_by_11 0x56w = 0x7Cw) /\
   (GF256_by_11 0x57w = 0x77w) /\
   (GF256_by_11 0x58w = 0x1Ew) /\
   (GF256_by_11 0x59w = 0x15w) /\
   (GF256_by_11 0x5Aw = 0x8w)  /\
   (GF256_by_11 0x5Bw = 0x3w)  /\
   (GF256_by_11 0x5Cw = 0x32w) /\
   (GF256_by_11 0x5Dw = 0x39w) /\
   (GF256_by_11 0x5Ew = 0x24w) /\
   (GF256_by_11 0x5Fw = 0x2Fw) /\
   (GF256_by_11 0x60w = 0x8Dw) /\
   (GF256_by_11 0x61w = 0x86w) /\
   (GF256_by_11 0x62w = 0x9Bw) /\
   (GF256_by_11 0x63w = 0x90w) /\
   (GF256_by_11 0x64w = 0xA1w) /\
   (GF256_by_11 0x65w = 0xAAw) /\
   (GF256_by_11 0x66w = 0xB7w) /\
   (GF256_by_11 0x67w = 0xBCw) /\
   (GF256_by_11 0x68w = 0xD5w) /\
   (GF256_by_11 0x69w = 0xDEw) /\
   (GF256_by_11 0x6Aw = 0xC3w) /\
   (GF256_by_11 0x6Bw = 0xC8w) /\
   (GF256_by_11 0x6Cw = 0xF9w) /\
   (GF256_by_11 0x6Dw = 0xF2w) /\
   (GF256_by_11 0x6Ew = 0xEFw) /\
   (GF256_by_11 0x6Fw = 0xE4w) /\
   (GF256_by_11 0x70w = 0x3Dw) /\
   (GF256_by_11 0x71w = 0x36w) /\
   (GF256_by_11 0x72w = 0x2Bw) /\
   (GF256_by_11 0x73w = 0x20w) /\
   (GF256_by_11 0x74w = 0x11w) /\
   (GF256_by_11 0x75w = 0x1Aw) /\
   (GF256_by_11 0x76w = 0x7w)  /\
   (GF256_by_11 0x77w = 0xCw)  /\
   (GF256_by_11 0x78w = 0x65w) /\
   (GF256_by_11 0x79w = 0x6Ew) /\
   (GF256_by_11 0x7Aw = 0x73w) /\
   (GF256_by_11 0x7Bw = 0x78w) /\
   (GF256_by_11 0x7Cw = 0x49w) /\
   (GF256_by_11 0x7Dw = 0x42w) /\
   (GF256_by_11 0x7Ew = 0x5Fw) /\
   (GF256_by_11 0x7Fw = 0x54w) /\
   (GF256_by_11 0x80w = 0xF7w) /\
   (GF256_by_11 0x81w = 0xFCw) /\
   (GF256_by_11 0x82w = 0xE1w) /\
   (GF256_by_11 0x83w = 0xEAw) /\
   (GF256_by_11 0x84w = 0xDBw) /\
   (GF256_by_11 0x85w = 0xD0w) /\
   (GF256_by_11 0x86w = 0xCDw) /\
   (GF256_by_11 0x87w = 0xC6w) /\
   (GF256_by_11 0x88w = 0xAFw) /\
   (GF256_by_11 0x89w = 0xA4w) /\
   (GF256_by_11 0x8Aw = 0xB9w) /\
   (GF256_by_11 0x8Bw = 0xB2w) /\
   (GF256_by_11 0x8Cw = 0x83w) /\
   (GF256_by_11 0x8Dw = 0x88w) /\
   (GF256_by_11 0x8Ew = 0x95w) /\
   (GF256_by_11 0x8Fw = 0x9Ew) /\
   (GF256_by_11 0x90w = 0x47w) /\
   (GF256_by_11 0x91w = 0x4Cw) /\
   (GF256_by_11 0x92w = 0x51w) /\
   (GF256_by_11 0x93w = 0x5Aw) /\
   (GF256_by_11 0x94w = 0x6Bw) /\
   (GF256_by_11 0x95w = 0x60w) /\
   (GF256_by_11 0x96w = 0x7Dw) /\
   (GF256_by_11 0x97w = 0x76w) /\
   (GF256_by_11 0x98w = 0x1Fw) /\
   (GF256_by_11 0x99w = 0x14w) /\
   (GF256_by_11 0x9Aw = 0x9w)  /\
   (GF256_by_11 0x9Bw = 0x2w)  /\
   (GF256_by_11 0x9Cw = 0x33w) /\
   (GF256_by_11 0x9Dw = 0x38w) /\
   (GF256_by_11 0x9Ew = 0x25w) /\
   (GF256_by_11 0x9Fw = 0x2Ew) /\
   (GF256_by_11 0xA0w = 0x8Cw) /\
   (GF256_by_11 0xA1w = 0x87w) /\
   (GF256_by_11 0xA2w = 0x9Aw) /\
   (GF256_by_11 0xA3w = 0x91w) /\
   (GF256_by_11 0xA4w = 0xA0w) /\
   (GF256_by_11 0xA5w = 0xABw) /\
   (GF256_by_11 0xA6w = 0xB6w) /\
   (GF256_by_11 0xA7w = 0xBDw) /\
   (GF256_by_11 0xA8w = 0xD4w) /\
   (GF256_by_11 0xA9w = 0xDFw) /\
   (GF256_by_11 0xAAw = 0xC2w) /\
   (GF256_by_11 0xABw = 0xC9w) /\
   (GF256_by_11 0xACw = 0xF8w) /\
   (GF256_by_11 0xADw = 0xF3w) /\
   (GF256_by_11 0xAEw = 0xEEw) /\
   (GF256_by_11 0xAFw = 0xE5w) /\
   (GF256_by_11 0xB0w = 0x3Cw) /\
   (GF256_by_11 0xB1w = 0x37w) /\
   (GF256_by_11 0xB2w = 0x2Aw) /\
   (GF256_by_11 0xB3w = 0x21w) /\
   (GF256_by_11 0xB4w = 0x10w) /\
   (GF256_by_11 0xB5w = 0x1Bw) /\
   (GF256_by_11 0xB6w = 0x6w)  /\
   (GF256_by_11 0xB7w = 0xDw)  /\
   (GF256_by_11 0xB8w = 0x64w) /\
   (GF256_by_11 0xB9w = 0x6Fw) /\
   (GF256_by_11 0xBAw = 0x72w) /\
   (GF256_by_11 0xBBw = 0x79w) /\
   (GF256_by_11 0xBCw = 0x48w) /\
   (GF256_by_11 0xBDw = 0x43w) /\
   (GF256_by_11 0xBEw = 0x5Ew) /\
   (GF256_by_11 0xBFw = 0x55w) /\
   (GF256_by_11 0xC0w = 0x1w)  /\
   (GF256_by_11 0xC1w = 0xAw)  /\
   (GF256_by_11 0xC2w = 0x17w) /\
   (GF256_by_11 0xC3w = 0x1Cw) /\
   (GF256_by_11 0xC4w = 0x2Dw) /\
   (GF256_by_11 0xC5w = 0x26w) /\
   (GF256_by_11 0xC6w = 0x3Bw) /\
   (GF256_by_11 0xC7w = 0x30w) /\
   (GF256_by_11 0xC8w = 0x59w) /\
   (GF256_by_11 0xC9w = 0x52w) /\
   (GF256_by_11 0xCAw = 0x4Fw) /\
   (GF256_by_11 0xCBw = 0x44w) /\
   (GF256_by_11 0xCCw = 0x75w) /\
   (GF256_by_11 0xCDw = 0x7Ew) /\
   (GF256_by_11 0xCEw = 0x63w) /\
   (GF256_by_11 0xCFw = 0x68w) /\
   (GF256_by_11 0xD0w = 0xB1w) /\
   (GF256_by_11 0xD1w = 0xBAw) /\
   (GF256_by_11 0xD2w = 0xA7w) /\
   (GF256_by_11 0xD3w = 0xACw) /\
   (GF256_by_11 0xD4w = 0x9Dw) /\
   (GF256_by_11 0xD5w = 0x96w) /\
   (GF256_by_11 0xD6w = 0x8Bw) /\
   (GF256_by_11 0xD7w = 0x80w) /\
   (GF256_by_11 0xD8w = 0xE9w) /\
   (GF256_by_11 0xD9w = 0xE2w) /\
   (GF256_by_11 0xDAw = 0xFFw) /\
   (GF256_by_11 0xDBw = 0xF4w) /\
   (GF256_by_11 0xDCw = 0xC5w) /\
   (GF256_by_11 0xDDw = 0xCEw) /\
   (GF256_by_11 0xDEw = 0xD3w) /\
   (GF256_by_11 0xDFw = 0xD8w) /\
   (GF256_by_11 0xE0w = 0x7Aw) /\
   (GF256_by_11 0xE1w = 0x71w) /\
   (GF256_by_11 0xE2w = 0x6Cw) /\
   (GF256_by_11 0xE3w = 0x67w) /\
   (GF256_by_11 0xE4w = 0x56w) /\
   (GF256_by_11 0xE5w = 0x5Dw) /\
   (GF256_by_11 0xE6w = 0x40w) /\
   (GF256_by_11 0xE7w = 0x4Bw) /\
   (GF256_by_11 0xE8w = 0x22w) /\
   (GF256_by_11 0xE9w = 0x29w) /\
   (GF256_by_11 0xEAw = 0x34w) /\
   (GF256_by_11 0xEBw = 0x3Fw) /\
   (GF256_by_11 0xECw = 0xEw)  /\
   (GF256_by_11 0xEDw = 0x5w)  /\
   (GF256_by_11 0xEEw = 0x18w) /\
   (GF256_by_11 0xEFw = 0x13w) /\
   (GF256_by_11 0xF0w = 0xCAw) /\
   (GF256_by_11 0xF1w = 0xC1w) /\
   (GF256_by_11 0xF2w = 0xDCw) /\
   (GF256_by_11 0xF3w = 0xD7w) /\
   (GF256_by_11 0xF4w = 0xE6w) /\
   (GF256_by_11 0xF5w = 0xEDw) /\
   (GF256_by_11 0xF6w = 0xF0w) /\
   (GF256_by_11 0xF7w = 0xFBw) /\
   (GF256_by_11 0xF8w = 0x92w) /\
   (GF256_by_11 0xF9w = 0x99w) /\
   (GF256_by_11 0xFAw = 0x84w) /\
   (GF256_by_11 0xFBw = 0x8Fw) /\
   (GF256_by_11 0xFCw = 0xBEw) /\
   (GF256_by_11 0xFDw = 0xB5w) /\
   (GF256_by_11 0xFEw = 0xA8w) /\
   (GF256_by_11 0xFFw = 0xA3w)`;

val GF256_by_13 = Count.apply word8Define
  `(GF256_by_13 0x0w = 0x0w)  /\
   (GF256_by_13 0x1w = 0xDw)  /\
   (GF256_by_13 0x2w = 0x1Aw) /\
   (GF256_by_13 0x3w = 0x17w) /\
   (GF256_by_13 0x4w = 0x34w) /\
   (GF256_by_13 0x5w = 0x39w) /\
   (GF256_by_13 0x6w = 0x2Ew) /\
   (GF256_by_13 0x7w = 0x23w) /\
   (GF256_by_13 0x8w = 0x68w) /\
   (GF256_by_13 0x9w = 0x65w) /\
   (GF256_by_13 0xAw = 0x72w) /\
   (GF256_by_13 0xBw = 0x7Fw) /\
   (GF256_by_13 0xCw = 0x5Cw) /\
   (GF256_by_13 0xDw = 0x51w) /\
   (GF256_by_13 0xEw = 0x46w) /\
   (GF256_by_13 0xFw = 0x4Bw) /\
   (GF256_by_13 0x10w = 0xD0w) /\
   (GF256_by_13 0x11w = 0xDDw) /\
   (GF256_by_13 0x12w = 0xCAw) /\
   (GF256_by_13 0x13w = 0xC7w) /\
   (GF256_by_13 0x14w = 0xE4w) /\
   (GF256_by_13 0x15w = 0xE9w) /\
   (GF256_by_13 0x16w = 0xFEw) /\
   (GF256_by_13 0x17w = 0xF3w) /\
   (GF256_by_13 0x18w = 0xB8w) /\
   (GF256_by_13 0x19w = 0xB5w) /\
   (GF256_by_13 0x1Aw = 0xA2w) /\
   (GF256_by_13 0x1Bw = 0xAFw) /\
   (GF256_by_13 0x1Cw = 0x8Cw) /\
   (GF256_by_13 0x1Dw = 0x81w) /\
   (GF256_by_13 0x1Ew = 0x96w) /\
   (GF256_by_13 0x1Fw = 0x9Bw) /\
   (GF256_by_13 0x20w = 0xBBw) /\
   (GF256_by_13 0x21w = 0xB6w) /\
   (GF256_by_13 0x22w = 0xA1w) /\
   (GF256_by_13 0x23w = 0xACw) /\
   (GF256_by_13 0x24w = 0x8Fw) /\
   (GF256_by_13 0x25w = 0x82w) /\
   (GF256_by_13 0x26w = 0x95w) /\
   (GF256_by_13 0x27w = 0x98w) /\
   (GF256_by_13 0x28w = 0xD3w) /\
   (GF256_by_13 0x29w = 0xDEw) /\
   (GF256_by_13 0x2Aw = 0xC9w) /\
   (GF256_by_13 0x2Bw = 0xC4w) /\
   (GF256_by_13 0x2Cw = 0xE7w) /\
   (GF256_by_13 0x2Dw = 0xEAw) /\
   (GF256_by_13 0x2Ew = 0xFDw) /\
   (GF256_by_13 0x2Fw = 0xF0w) /\
   (GF256_by_13 0x30w = 0x6Bw) /\
   (GF256_by_13 0x31w = 0x66w) /\
   (GF256_by_13 0x32w = 0x71w) /\
   (GF256_by_13 0x33w = 0x7Cw) /\
   (GF256_by_13 0x34w = 0x5Fw) /\
   (GF256_by_13 0x35w = 0x52w) /\
   (GF256_by_13 0x36w = 0x45w) /\
   (GF256_by_13 0x37w = 0x48w) /\
   (GF256_by_13 0x38w = 0x3w)  /\
   (GF256_by_13 0x39w = 0xEw)  /\
   (GF256_by_13 0x3Aw = 0x19w) /\
   (GF256_by_13 0x3Bw = 0x14w) /\
   (GF256_by_13 0x3Cw = 0x37w) /\
   (GF256_by_13 0x3Dw = 0x3Aw) /\
   (GF256_by_13 0x3Ew = 0x2Dw) /\
   (GF256_by_13 0x3Fw = 0x20w) /\
   (GF256_by_13 0x40w = 0x6Dw) /\
   (GF256_by_13 0x41w = 0x60w) /\
   (GF256_by_13 0x42w = 0x77w) /\
   (GF256_by_13 0x43w = 0x7Aw) /\
   (GF256_by_13 0x44w = 0x59w) /\
   (GF256_by_13 0x45w = 0x54w) /\
   (GF256_by_13 0x46w = 0x43w) /\
   (GF256_by_13 0x47w = 0x4Ew) /\
   (GF256_by_13 0x48w = 0x5w)  /\
   (GF256_by_13 0x49w = 0x8w)  /\
   (GF256_by_13 0x4Aw = 0x1Fw) /\
   (GF256_by_13 0x4Bw = 0x12w) /\
   (GF256_by_13 0x4Cw = 0x31w) /\
   (GF256_by_13 0x4Dw = 0x3Cw) /\
   (GF256_by_13 0x4Ew = 0x2Bw) /\
   (GF256_by_13 0x4Fw = 0x26w) /\
   (GF256_by_13 0x50w = 0xBDw) /\
   (GF256_by_13 0x51w = 0xB0w) /\
   (GF256_by_13 0x52w = 0xA7w) /\
   (GF256_by_13 0x53w = 0xAAw) /\
   (GF256_by_13 0x54w = 0x89w) /\
   (GF256_by_13 0x55w = 0x84w) /\
   (GF256_by_13 0x56w = 0x93w) /\
   (GF256_by_13 0x57w = 0x9Ew) /\
   (GF256_by_13 0x58w = 0xD5w) /\
   (GF256_by_13 0x59w = 0xD8w) /\
   (GF256_by_13 0x5Aw = 0xCFw) /\
   (GF256_by_13 0x5Bw = 0xC2w) /\
   (GF256_by_13 0x5Cw = 0xE1w) /\
   (GF256_by_13 0x5Dw = 0xECw) /\
   (GF256_by_13 0x5Ew = 0xFBw) /\
   (GF256_by_13 0x5Fw = 0xF6w) /\
   (GF256_by_13 0x60w = 0xD6w) /\
   (GF256_by_13 0x61w = 0xDBw) /\
   (GF256_by_13 0x62w = 0xCCw) /\
   (GF256_by_13 0x63w = 0xC1w) /\
   (GF256_by_13 0x64w = 0xE2w) /\
   (GF256_by_13 0x65w = 0xEFw) /\
   (GF256_by_13 0x66w = 0xF8w) /\
   (GF256_by_13 0x67w = 0xF5w) /\
   (GF256_by_13 0x68w = 0xBEw) /\
   (GF256_by_13 0x69w = 0xB3w) /\
   (GF256_by_13 0x6Aw = 0xA4w) /\
   (GF256_by_13 0x6Bw = 0xA9w) /\
   (GF256_by_13 0x6Cw = 0x8Aw) /\
   (GF256_by_13 0x6Dw = 0x87w) /\
   (GF256_by_13 0x6Ew = 0x90w) /\
   (GF256_by_13 0x6Fw = 0x9Dw) /\
   (GF256_by_13 0x70w = 0x6w)  /\
   (GF256_by_13 0x71w = 0xBw)  /\
   (GF256_by_13 0x72w = 0x1Cw) /\
   (GF256_by_13 0x73w = 0x11w) /\
   (GF256_by_13 0x74w = 0x32w) /\
   (GF256_by_13 0x75w = 0x3Fw) /\
   (GF256_by_13 0x76w = 0x28w) /\
   (GF256_by_13 0x77w = 0x25w) /\
   (GF256_by_13 0x78w = 0x6Ew) /\
   (GF256_by_13 0x79w = 0x63w) /\
   (GF256_by_13 0x7Aw = 0x74w) /\
   (GF256_by_13 0x7Bw = 0x79w) /\
   (GF256_by_13 0x7Cw = 0x5Aw) /\
   (GF256_by_13 0x7Dw = 0x57w) /\
   (GF256_by_13 0x7Ew = 0x40w) /\
   (GF256_by_13 0x7Fw = 0x4Dw) /\
   (GF256_by_13 0x80w = 0xDAw) /\
   (GF256_by_13 0x81w = 0xD7w) /\
   (GF256_by_13 0x82w = 0xC0w) /\
   (GF256_by_13 0x83w = 0xCDw) /\
   (GF256_by_13 0x84w = 0xEEw) /\
   (GF256_by_13 0x85w = 0xE3w) /\
   (GF256_by_13 0x86w = 0xF4w) /\
   (GF256_by_13 0x87w = 0xF9w) /\
   (GF256_by_13 0x88w = 0xB2w) /\
   (GF256_by_13 0x89w = 0xBFw) /\
   (GF256_by_13 0x8Aw = 0xA8w) /\
   (GF256_by_13 0x8Bw = 0xA5w) /\
   (GF256_by_13 0x8Cw = 0x86w) /\
   (GF256_by_13 0x8Dw = 0x8Bw) /\
   (GF256_by_13 0x8Ew = 0x9Cw) /\
   (GF256_by_13 0x8Fw = 0x91w) /\
   (GF256_by_13 0x90w = 0xAw)  /\
   (GF256_by_13 0x91w = 0x7w)  /\
   (GF256_by_13 0x92w = 0x10w) /\
   (GF256_by_13 0x93w = 0x1Dw) /\
   (GF256_by_13 0x94w = 0x3Ew) /\
   (GF256_by_13 0x95w = 0x33w) /\
   (GF256_by_13 0x96w = 0x24w) /\
   (GF256_by_13 0x97w = 0x29w) /\
   (GF256_by_13 0x98w = 0x62w) /\
   (GF256_by_13 0x99w = 0x6Fw) /\
   (GF256_by_13 0x9Aw = 0x78w) /\
   (GF256_by_13 0x9Bw = 0x75w) /\
   (GF256_by_13 0x9Cw = 0x56w) /\
   (GF256_by_13 0x9Dw = 0x5Bw) /\
   (GF256_by_13 0x9Ew = 0x4Cw) /\
   (GF256_by_13 0x9Fw = 0x41w) /\
   (GF256_by_13 0xA0w = 0x61w) /\
   (GF256_by_13 0xA1w = 0x6Cw) /\
   (GF256_by_13 0xA2w = 0x7Bw) /\
   (GF256_by_13 0xA3w = 0x76w) /\
   (GF256_by_13 0xA4w = 0x55w) /\
   (GF256_by_13 0xA5w = 0x58w) /\
   (GF256_by_13 0xA6w = 0x4Fw) /\
   (GF256_by_13 0xA7w = 0x42w) /\
   (GF256_by_13 0xA8w = 0x9w)  /\
   (GF256_by_13 0xA9w = 0x4w)  /\
   (GF256_by_13 0xAAw = 0x13w) /\
   (GF256_by_13 0xABw = 0x1Ew) /\
   (GF256_by_13 0xACw = 0x3Dw) /\
   (GF256_by_13 0xADw = 0x30w) /\
   (GF256_by_13 0xAEw = 0x27w) /\
   (GF256_by_13 0xAFw = 0x2Aw) /\
   (GF256_by_13 0xB0w = 0xB1w) /\
   (GF256_by_13 0xB1w = 0xBCw) /\
   (GF256_by_13 0xB2w = 0xABw) /\
   (GF256_by_13 0xB3w = 0xA6w) /\
   (GF256_by_13 0xB4w = 0x85w) /\
   (GF256_by_13 0xB5w = 0x88w) /\
   (GF256_by_13 0xB6w = 0x9Fw) /\
   (GF256_by_13 0xB7w = 0x92w) /\
   (GF256_by_13 0xB8w = 0xD9w) /\
   (GF256_by_13 0xB9w = 0xD4w) /\
   (GF256_by_13 0xBAw = 0xC3w) /\
   (GF256_by_13 0xBBw = 0xCEw) /\
   (GF256_by_13 0xBCw = 0xEDw) /\
   (GF256_by_13 0xBDw = 0xE0w) /\
   (GF256_by_13 0xBEw = 0xF7w) /\
   (GF256_by_13 0xBFw = 0xFAw) /\
   (GF256_by_13 0xC0w = 0xB7w) /\
   (GF256_by_13 0xC1w = 0xBAw) /\
   (GF256_by_13 0xC2w = 0xADw) /\
   (GF256_by_13 0xC3w = 0xA0w) /\
   (GF256_by_13 0xC4w = 0x83w) /\
   (GF256_by_13 0xC5w = 0x8Ew) /\
   (GF256_by_13 0xC6w = 0x99w) /\
   (GF256_by_13 0xC7w = 0x94w) /\
   (GF256_by_13 0xC8w = 0xDFw) /\
   (GF256_by_13 0xC9w = 0xD2w) /\
   (GF256_by_13 0xCAw = 0xC5w) /\
   (GF256_by_13 0xCBw = 0xC8w) /\
   (GF256_by_13 0xCCw = 0xEBw) /\
   (GF256_by_13 0xCDw = 0xE6w) /\
   (GF256_by_13 0xCEw = 0xF1w) /\
   (GF256_by_13 0xCFw = 0xFCw) /\
   (GF256_by_13 0xD0w = 0x67w) /\
   (GF256_by_13 0xD1w = 0x6Aw) /\
   (GF256_by_13 0xD2w = 0x7Dw) /\
   (GF256_by_13 0xD3w = 0x70w) /\
   (GF256_by_13 0xD4w = 0x53w) /\
   (GF256_by_13 0xD5w = 0x5Ew) /\
   (GF256_by_13 0xD6w = 0x49w) /\
   (GF256_by_13 0xD7w = 0x44w) /\
   (GF256_by_13 0xD8w = 0xFw)  /\
   (GF256_by_13 0xD9w = 0x2w)  /\
   (GF256_by_13 0xDAw = 0x15w) /\
   (GF256_by_13 0xDBw = 0x18w) /\
   (GF256_by_13 0xDCw = 0x3Bw) /\
   (GF256_by_13 0xDDw = 0x36w) /\
   (GF256_by_13 0xDEw = 0x21w) /\
   (GF256_by_13 0xDFw = 0x2Cw) /\
   (GF256_by_13 0xE0w = 0xCw)  /\
   (GF256_by_13 0xE1w = 0x1w)  /\
   (GF256_by_13 0xE2w = 0x16w) /\
   (GF256_by_13 0xE3w = 0x1Bw) /\
   (GF256_by_13 0xE4w = 0x38w) /\
   (GF256_by_13 0xE5w = 0x35w) /\
   (GF256_by_13 0xE6w = 0x22w) /\
   (GF256_by_13 0xE7w = 0x2Fw) /\
   (GF256_by_13 0xE8w = 0x64w) /\
   (GF256_by_13 0xE9w = 0x69w) /\
   (GF256_by_13 0xEAw = 0x7Ew) /\
   (GF256_by_13 0xEBw = 0x73w) /\
   (GF256_by_13 0xECw = 0x50w) /\
   (GF256_by_13 0xEDw = 0x5Dw) /\
   (GF256_by_13 0xEEw = 0x4Aw) /\
   (GF256_by_13 0xEFw = 0x47w) /\
   (GF256_by_13 0xF0w = 0xDCw) /\
   (GF256_by_13 0xF1w = 0xD1w) /\
   (GF256_by_13 0xF2w = 0xC6w) /\
   (GF256_by_13 0xF3w = 0xCBw) /\
   (GF256_by_13 0xF4w = 0xE8w) /\
   (GF256_by_13 0xF5w = 0xE5w) /\
   (GF256_by_13 0xF6w = 0xF2w) /\
   (GF256_by_13 0xF7w = 0xFFw) /\
   (GF256_by_13 0xF8w = 0xB4w) /\
   (GF256_by_13 0xF9w = 0xB9w) /\
   (GF256_by_13 0xFAw = 0xAEw) /\
   (GF256_by_13 0xFBw = 0xA3w) /\
   (GF256_by_13 0xFCw = 0x80w) /\
   (GF256_by_13 0xFDw = 0x8Dw) /\
   (GF256_by_13 0xFEw = 0x9Aw) /\
   (GF256_by_13 0xFFw = 0x97w)`;

val GF256_by_14 = Count.apply word8Define
  `(GF256_by_14 0x0w = 0x0w)  /\
   (GF256_by_14 0x1w = 0xEw)  /\
   (GF256_by_14 0x2w = 0x1Cw) /\
   (GF256_by_14 0x3w = 0x12w) /\
   (GF256_by_14 0x4w = 0x38w) /\
   (GF256_by_14 0x5w = 0x36w) /\
   (GF256_by_14 0x6w = 0x24w) /\
   (GF256_by_14 0x7w = 0x2Aw) /\
   (GF256_by_14 0x8w = 0x70w) /\
   (GF256_by_14 0x9w = 0x7Ew) /\
   (GF256_by_14 0xAw = 0x6Cw) /\
   (GF256_by_14 0xBw = 0x62w) /\
   (GF256_by_14 0xCw = 0x48w) /\
   (GF256_by_14 0xDw = 0x46w) /\
   (GF256_by_14 0xEw = 0x54w) /\
   (GF256_by_14 0xFw = 0x5Aw) /\
   (GF256_by_14 0x10w = 0xE0w) /\
   (GF256_by_14 0x11w = 0xEEw) /\
   (GF256_by_14 0x12w = 0xFCw) /\
   (GF256_by_14 0x13w = 0xF2w) /\
   (GF256_by_14 0x14w = 0xD8w) /\
   (GF256_by_14 0x15w = 0xD6w) /\
   (GF256_by_14 0x16w = 0xC4w) /\
   (GF256_by_14 0x17w = 0xCAw) /\
   (GF256_by_14 0x18w = 0x90w) /\
   (GF256_by_14 0x19w = 0x9Ew) /\
   (GF256_by_14 0x1Aw = 0x8Cw) /\
   (GF256_by_14 0x1Bw = 0x82w) /\
   (GF256_by_14 0x1Cw = 0xA8w) /\
   (GF256_by_14 0x1Dw = 0xA6w) /\
   (GF256_by_14 0x1Ew = 0xB4w) /\
   (GF256_by_14 0x1Fw = 0xBAw) /\
   (GF256_by_14 0x20w = 0xDBw) /\
   (GF256_by_14 0x21w = 0xD5w) /\
   (GF256_by_14 0x22w = 0xC7w) /\
   (GF256_by_14 0x23w = 0xC9w) /\
   (GF256_by_14 0x24w = 0xE3w) /\
   (GF256_by_14 0x25w = 0xEDw) /\
   (GF256_by_14 0x26w = 0xFFw) /\
   (GF256_by_14 0x27w = 0xF1w) /\
   (GF256_by_14 0x28w = 0xABw) /\
   (GF256_by_14 0x29w = 0xA5w) /\
   (GF256_by_14 0x2Aw = 0xB7w) /\
   (GF256_by_14 0x2Bw = 0xB9w) /\
   (GF256_by_14 0x2Cw = 0x93w) /\
   (GF256_by_14 0x2Dw = 0x9Dw) /\
   (GF256_by_14 0x2Ew = 0x8Fw) /\
   (GF256_by_14 0x2Fw = 0x81w) /\
   (GF256_by_14 0x30w = 0x3Bw) /\
   (GF256_by_14 0x31w = 0x35w) /\
   (GF256_by_14 0x32w = 0x27w) /\
   (GF256_by_14 0x33w = 0x29w) /\
   (GF256_by_14 0x34w = 0x3w)  /\
   (GF256_by_14 0x35w = 0xDw)  /\
   (GF256_by_14 0x36w = 0x1Fw) /\
   (GF256_by_14 0x37w = 0x11w) /\
   (GF256_by_14 0x38w = 0x4Bw) /\
   (GF256_by_14 0x39w = 0x45w) /\
   (GF256_by_14 0x3Aw = 0x57w) /\
   (GF256_by_14 0x3Bw = 0x59w) /\
   (GF256_by_14 0x3Cw = 0x73w) /\
   (GF256_by_14 0x3Dw = 0x7Dw) /\
   (GF256_by_14 0x3Ew = 0x6Fw) /\
   (GF256_by_14 0x3Fw = 0x61w) /\
   (GF256_by_14 0x40w = 0xADw) /\
   (GF256_by_14 0x41w = 0xA3w) /\
   (GF256_by_14 0x42w = 0xB1w) /\
   (GF256_by_14 0x43w = 0xBFw) /\
   (GF256_by_14 0x44w = 0x95w) /\
   (GF256_by_14 0x45w = 0x9Bw) /\
   (GF256_by_14 0x46w = 0x89w) /\
   (GF256_by_14 0x47w = 0x87w) /\
   (GF256_by_14 0x48w = 0xDDw) /\
   (GF256_by_14 0x49w = 0xD3w) /\
   (GF256_by_14 0x4Aw = 0xC1w) /\
   (GF256_by_14 0x4Bw = 0xCFw) /\
   (GF256_by_14 0x4Cw = 0xE5w) /\
   (GF256_by_14 0x4Dw = 0xEBw) /\
   (GF256_by_14 0x4Ew = 0xF9w) /\
   (GF256_by_14 0x4Fw = 0xF7w) /\
   (GF256_by_14 0x50w = 0x4Dw) /\
   (GF256_by_14 0x51w = 0x43w) /\
   (GF256_by_14 0x52w = 0x51w) /\
   (GF256_by_14 0x53w = 0x5Fw) /\
   (GF256_by_14 0x54w = 0x75w) /\
   (GF256_by_14 0x55w = 0x7Bw) /\
   (GF256_by_14 0x56w = 0x69w) /\
   (GF256_by_14 0x57w = 0x67w) /\
   (GF256_by_14 0x58w = 0x3Dw) /\
   (GF256_by_14 0x59w = 0x33w) /\
   (GF256_by_14 0x5Aw = 0x21w) /\
   (GF256_by_14 0x5Bw = 0x2Fw) /\
   (GF256_by_14 0x5Cw = 0x5w)  /\
   (GF256_by_14 0x5Dw = 0xBw)  /\
   (GF256_by_14 0x5Ew = 0x19w) /\
   (GF256_by_14 0x5Fw = 0x17w) /\
   (GF256_by_14 0x60w = 0x76w) /\
   (GF256_by_14 0x61w = 0x78w) /\
   (GF256_by_14 0x62w = 0x6Aw) /\
   (GF256_by_14 0x63w = 0x64w) /\
   (GF256_by_14 0x64w = 0x4Ew) /\
   (GF256_by_14 0x65w = 0x40w) /\
   (GF256_by_14 0x66w = 0x52w) /\
   (GF256_by_14 0x67w = 0x5Cw) /\
   (GF256_by_14 0x68w = 0x6w)  /\
   (GF256_by_14 0x69w = 0x8w)  /\
   (GF256_by_14 0x6Aw = 0x1Aw) /\
   (GF256_by_14 0x6Bw = 0x14w) /\
   (GF256_by_14 0x6Cw = 0x3Ew) /\
   (GF256_by_14 0x6Dw = 0x30w) /\
   (GF256_by_14 0x6Ew = 0x22w) /\
   (GF256_by_14 0x6Fw = 0x2Cw) /\
   (GF256_by_14 0x70w = 0x96w) /\
   (GF256_by_14 0x71w = 0x98w) /\
   (GF256_by_14 0x72w = 0x8Aw) /\
   (GF256_by_14 0x73w = 0x84w) /\
   (GF256_by_14 0x74w = 0xAEw) /\
   (GF256_by_14 0x75w = 0xA0w) /\
   (GF256_by_14 0x76w = 0xB2w) /\
   (GF256_by_14 0x77w = 0xBCw) /\
   (GF256_by_14 0x78w = 0xE6w) /\
   (GF256_by_14 0x79w = 0xE8w) /\
   (GF256_by_14 0x7Aw = 0xFAw) /\
   (GF256_by_14 0x7Bw = 0xF4w) /\
   (GF256_by_14 0x7Cw = 0xDEw) /\
   (GF256_by_14 0x7Dw = 0xD0w) /\
   (GF256_by_14 0x7Ew = 0xC2w) /\
   (GF256_by_14 0x7Fw = 0xCCw) /\
   (GF256_by_14 0x80w = 0x41w) /\
   (GF256_by_14 0x81w = 0x4Fw) /\
   (GF256_by_14 0x82w = 0x5Dw) /\
   (GF256_by_14 0x83w = 0x53w) /\
   (GF256_by_14 0x84w = 0x79w) /\
   (GF256_by_14 0x85w = 0x77w) /\
   (GF256_by_14 0x86w = 0x65w) /\
   (GF256_by_14 0x87w = 0x6Bw) /\
   (GF256_by_14 0x88w = 0x31w) /\
   (GF256_by_14 0x89w = 0x3Fw) /\
   (GF256_by_14 0x8Aw = 0x2Dw) /\
   (GF256_by_14 0x8Bw = 0x23w) /\
   (GF256_by_14 0x8Cw = 0x9w)  /\
   (GF256_by_14 0x8Dw = 0x7w)  /\
   (GF256_by_14 0x8Ew = 0x15w) /\
   (GF256_by_14 0x8Fw = 0x1Bw) /\
   (GF256_by_14 0x90w = 0xA1w) /\
   (GF256_by_14 0x91w = 0xAFw) /\
   (GF256_by_14 0x92w = 0xBDw) /\
   (GF256_by_14 0x93w = 0xB3w) /\
   (GF256_by_14 0x94w = 0x99w) /\
   (GF256_by_14 0x95w = 0x97w) /\
   (GF256_by_14 0x96w = 0x85w) /\
   (GF256_by_14 0x97w = 0x8Bw) /\
   (GF256_by_14 0x98w = 0xD1w) /\
   (GF256_by_14 0x99w = 0xDFw) /\
   (GF256_by_14 0x9Aw = 0xCDw) /\
   (GF256_by_14 0x9Bw = 0xC3w) /\
   (GF256_by_14 0x9Cw = 0xE9w) /\
   (GF256_by_14 0x9Dw = 0xE7w) /\
   (GF256_by_14 0x9Ew = 0xF5w) /\
   (GF256_by_14 0x9Fw = 0xFBw) /\
   (GF256_by_14 0xA0w = 0x9Aw) /\
   (GF256_by_14 0xA1w = 0x94w) /\
   (GF256_by_14 0xA2w = 0x86w) /\
   (GF256_by_14 0xA3w = 0x88w) /\
   (GF256_by_14 0xA4w = 0xA2w) /\
   (GF256_by_14 0xA5w = 0xACw) /\
   (GF256_by_14 0xA6w = 0xBEw) /\
   (GF256_by_14 0xA7w = 0xB0w) /\
   (GF256_by_14 0xA8w = 0xEAw) /\
   (GF256_by_14 0xA9w = 0xE4w) /\
   (GF256_by_14 0xAAw = 0xF6w) /\
   (GF256_by_14 0xABw = 0xF8w) /\
   (GF256_by_14 0xACw = 0xD2w) /\
   (GF256_by_14 0xADw = 0xDCw) /\
   (GF256_by_14 0xAEw = 0xCEw) /\
   (GF256_by_14 0xAFw = 0xC0w) /\
   (GF256_by_14 0xB0w = 0x7Aw) /\
   (GF256_by_14 0xB1w = 0x74w) /\
   (GF256_by_14 0xB2w = 0x66w) /\
   (GF256_by_14 0xB3w = 0x68w) /\
   (GF256_by_14 0xB4w = 0x42w) /\
   (GF256_by_14 0xB5w = 0x4Cw) /\
   (GF256_by_14 0xB6w = 0x5Ew) /\
   (GF256_by_14 0xB7w = 0x50w) /\
   (GF256_by_14 0xB8w = 0xAw)  /\
   (GF256_by_14 0xB9w = 0x4w)  /\
   (GF256_by_14 0xBAw = 0x16w) /\
   (GF256_by_14 0xBBw = 0x18w) /\
   (GF256_by_14 0xBCw = 0x32w) /\
   (GF256_by_14 0xBDw = 0x3Cw) /\
   (GF256_by_14 0xBEw = 0x2Ew) /\
   (GF256_by_14 0xBFw = 0x20w) /\
   (GF256_by_14 0xC0w = 0xECw) /\
   (GF256_by_14 0xC1w = 0xE2w) /\
   (GF256_by_14 0xC2w = 0xF0w) /\
   (GF256_by_14 0xC3w = 0xFEw) /\
   (GF256_by_14 0xC4w = 0xD4w) /\
   (GF256_by_14 0xC5w = 0xDAw) /\
   (GF256_by_14 0xC6w = 0xC8w) /\
   (GF256_by_14 0xC7w = 0xC6w) /\
   (GF256_by_14 0xC8w = 0x9Cw) /\
   (GF256_by_14 0xC9w = 0x92w) /\
   (GF256_by_14 0xCAw = 0x80w) /\
   (GF256_by_14 0xCBw = 0x8Ew) /\
   (GF256_by_14 0xCCw = 0xA4w) /\
   (GF256_by_14 0xCDw = 0xAAw) /\
   (GF256_by_14 0xCEw = 0xB8w) /\
   (GF256_by_14 0xCFw = 0xB6w) /\
   (GF256_by_14 0xD0w = 0xCw)  /\
   (GF256_by_14 0xD1w = 0x2w)  /\
   (GF256_by_14 0xD2w = 0x10w) /\
   (GF256_by_14 0xD3w = 0x1Ew) /\
   (GF256_by_14 0xD4w = 0x34w) /\
   (GF256_by_14 0xD5w = 0x3Aw) /\
   (GF256_by_14 0xD6w = 0x28w) /\
   (GF256_by_14 0xD7w = 0x26w) /\
   (GF256_by_14 0xD8w = 0x7Cw) /\
   (GF256_by_14 0xD9w = 0x72w) /\
   (GF256_by_14 0xDAw = 0x60w) /\
   (GF256_by_14 0xDBw = 0x6Ew) /\
   (GF256_by_14 0xDCw = 0x44w) /\
   (GF256_by_14 0xDDw = 0x4Aw) /\
   (GF256_by_14 0xDEw = 0x58w) /\
   (GF256_by_14 0xDFw = 0x56w) /\
   (GF256_by_14 0xE0w = 0x37w) /\
   (GF256_by_14 0xE1w = 0x39w) /\
   (GF256_by_14 0xE2w = 0x2Bw) /\
   (GF256_by_14 0xE3w = 0x25w) /\
   (GF256_by_14 0xE4w = 0xFw)  /\
   (GF256_by_14 0xE5w = 0x1w)  /\
   (GF256_by_14 0xE6w = 0x13w) /\
   (GF256_by_14 0xE7w = 0x1Dw) /\
   (GF256_by_14 0xE8w = 0x47w) /\
   (GF256_by_14 0xE9w = 0x49w) /\
   (GF256_by_14 0xEAw = 0x5Bw) /\
   (GF256_by_14 0xEBw = 0x55w) /\
   (GF256_by_14 0xECw = 0x7Fw) /\
   (GF256_by_14 0xEDw = 0x71w) /\
   (GF256_by_14 0xEEw = 0x63w) /\
   (GF256_by_14 0xEFw = 0x6Dw) /\
   (GF256_by_14 0xF0w = 0xD7w) /\
   (GF256_by_14 0xF1w = 0xD9w) /\
   (GF256_by_14 0xF2w = 0xCBw) /\
   (GF256_by_14 0xF3w = 0xC5w) /\
   (GF256_by_14 0xF4w = 0xEFw) /\
   (GF256_by_14 0xF5w = 0xE1w) /\
   (GF256_by_14 0xF6w = 0xF3w) /\
   (GF256_by_14 0xF7w = 0xFDw) /\
   (GF256_by_14 0xF8w = 0xA7w) /\
   (GF256_by_14 0xF9w = 0xA9w) /\
   (GF256_by_14 0xFAw = 0xBBw) /\
   (GF256_by_14 0xFBw = 0xB5w) /\
   (GF256_by_14 0xFCw = 0x9Fw) /\
   (GF256_by_14 0xFDw = 0x91w) /\
   (GF256_by_14 0xFEw = 0x83w) /\
   (GF256_by_14 0xFFw = 0x8Dw)`;

*)

val _ = export_theory();
